Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  sbequilem Unicode version

Theorem sbequilem 1818
 Description: Propositional logic lemma used in the sbequi 1819 proof. (Contributed by Jim Kingdon, 1-Feb-2018.)
Hypotheses
Ref Expression
sbequilem.1
sbequilem.2
Assertion
Ref Expression
sbequilem

Proof of Theorem sbequilem
StepHypRef Expression
1 sbequilem.1 . . . . . . . . . 10
2 sbequilem.2 . . . . . . . . . 10
31, 2pm3.2i 270 . . . . . . . . 9
4 andi 808 . . . . . . . . 9
53, 4mpbi 144 . . . . . . . 8
6 andir 809 . . . . . . . . 9
7 andir 809 . . . . . . . . 9
86, 7orbi12i 754 . . . . . . . 8
95, 8mpbi 144 . . . . . . 7
10 pm3.43 592 . . . . . . . . . 10
11 pm3.33 343 . . . . . . . . . 10
1210, 11syl6 33 . . . . . . . . 9
1312orim2i 751 . . . . . . . 8
1413orim2i 751 . . . . . . 7
159, 14ax-mp 5 . . . . . 6
16 simpr 109 . . . . . . . 8
176, 16sylbir 134 . . . . . . 7
1817orim1i 750 . . . . . 6
1915, 18ax-mp 5 . . . . 5
20 simpl 108 . . . . . . 7
2120orim1i 750 . . . . . 6
2221orim2i 751 . . . . 5
2319, 22ax-mp 5 . . . 4
24 orass 757 . . . 4
2523, 24mpbir 145 . . 3
26 orcom 718 . . . 4
2726orbi1i 753 . . 3
2825, 27mpbi 144 . 2
29 orass 757 . 2
3028, 29mpbi 144 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   wo 698 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  sbequi  1819
 Copyright terms: Public domain W3C validator