Original no-premise proof; forall x: Calgary TFL rules
Goal: (P -> Q) <-> ((P or Q) -> Q).
1 P -> Q                         AS, first direction
2 P or Q                         AS, nested conditional
3 P                              AS, first disjunction case
4 Q                              ->E 1,3
5 Q                              AS, sibling second case
6 Q                              Reiteration 5
7 Q                              or E 2,3-4,5-6
8 (P or Q) -> Q                  ->I 2-7
9 (P or Q) -> Q                  AS, sibling second direction
10 P                             AS, nested conditional
11 P or Q                        or I 10
12 Q                             ->E 9,11
13 P -> Q                        ->I 10-12
14 (P -> Q) <-> ((P or Q) -> Q)   <->I 1-8,9-13
Blocks: 1-8; 2-7; 3-4; 5-6; 9-13; 10-12.
Truth check P,Q: TT both sides T; TF both sides F; FT both sides T; FF both sides T. Biconditional T on all four rows.