Basically the bullet proofs leave out the meat of a proof and just give you the bones so

- Inside the
=<...>

we need only list the theorem, or theorem number, not forgetting our|-

and we need not mention the use of inference rules anywhere. - For style 4.1 we now do not need to worry about the part of the proof after the "=<...>" bit of the proof i.e. no need to mention transitivity, or the derived inference rules for
=>

at the end. - For the deduction theorem, if proving
|- P_1 ^P_2^...^P_n => Q

we only need to say "assume P_1, P_2,...,P_n" and then give a bullet proof of Q. That's all. - For proof by cases, since we don't mention substitutions in bullet proofs, just bullet prove the theorem with
*true*already substituted in, and then give a bullet prof of the theorem with*false*already substitued in. That's all.Remember to substitute the same variable each time.

- For the other types (contrapositive, contradiction etc) we are just trying to prove say A is a theorem, from which we can deduce B is a theorem by (contradiction, contrapositive, whatever). For this all we have to do is give a bullet proof that A is a theorem.