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

Theorem sbequilem 1719
Description: Propositional logic lemma used in the sbequi 1720 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 257 . . . . . . . . 9 ((𝜑 ∨ (𝜓 → (𝜒𝜃))) ∧ (𝜏 ∨ (𝜓 → (𝜃𝜂))))
4 andi 731 . . . . . . . . 9 (((𝜑 ∨ (𝜓 → (𝜒𝜃))) ∧ (𝜏 ∨ (𝜓 → (𝜃𝜂)))) ↔ (((𝜑 ∨ (𝜓 → (𝜒𝜃))) ∧ 𝜏) ∨ ((𝜑 ∨ (𝜓 → (𝜒𝜃))) ∧ (𝜓 → (𝜃𝜂)))))
53, 4mpbi 133 . . . . . . . 8 (((𝜑 ∨ (𝜓 → (𝜒𝜃))) ∧ 𝜏) ∨ ((𝜑 ∨ (𝜓 → (𝜒𝜃))) ∧ (𝜓 → (𝜃𝜂))))
6 andir 732 . . . . . . . . 9 (((𝜑 ∨ (𝜓 → (𝜒𝜃))) ∧ 𝜏) ↔ ((𝜑𝜏) ∨ ((𝜓 → (𝜒𝜃)) ∧ 𝜏)))
7 andir 732 . . . . . . . . 9 (((𝜑 ∨ (𝜓 → (𝜒𝜃))) ∧ (𝜓 → (𝜃𝜂))) ↔ ((𝜑 ∧ (𝜓 → (𝜃𝜂))) ∨ ((𝜓 → (𝜒𝜃)) ∧ (𝜓 → (𝜃𝜂)))))
86, 7orbi12i 681 . . . . . . . 8 ((((𝜑 ∨ (𝜓 → (𝜒𝜃))) ∧ 𝜏) ∨ ((𝜑 ∨ (𝜓 → (𝜒𝜃))) ∧ (𝜓 → (𝜃𝜂)))) ↔ (((𝜑𝜏) ∨ ((𝜓 → (𝜒𝜃)) ∧ 𝜏)) ∨ ((𝜑 ∧ (𝜓 → (𝜃𝜂))) ∨ ((𝜓 → (𝜒𝜃)) ∧ (𝜓 → (𝜃𝜂))))))
95, 8mpbi 133 . . . . . . 7 (((𝜑𝜏) ∨ ((𝜓 → (𝜒𝜃)) ∧ 𝜏)) ∨ ((𝜑 ∧ (𝜓 → (𝜃𝜂))) ∨ ((𝜓 → (𝜒𝜃)) ∧ (𝜓 → (𝜃𝜂)))))
10 pm3.43 534 . . . . . . . . . 10 (((𝜓 → (𝜒𝜃)) ∧ (𝜓 → (𝜃𝜂))) → (𝜓 → ((𝜒𝜃) ∧ (𝜃𝜂))))
11 pm3.33 327 . . . . . . . . . 10 (((𝜒𝜃) ∧ (𝜃𝜂)) → (𝜒𝜂))
1210, 11syl6 29 . . . . . . . . 9 (((𝜓 → (𝜒𝜃)) ∧ (𝜓 → (𝜃𝜂))) → (𝜓 → (𝜒𝜂)))
1312orim2i 678 . . . . . . . 8 (((𝜑 ∧ (𝜓 → (𝜃𝜂))) ∨ ((𝜓 → (𝜒𝜃)) ∧ (𝜓 → (𝜃𝜂)))) → ((𝜑 ∧ (𝜓 → (𝜃𝜂))) ∨ (𝜓 → (𝜒𝜂))))
1413orim2i 678 . . . . . . 7 ((((𝜑𝜏) ∨ ((𝜓 → (𝜒𝜃)) ∧ 𝜏)) ∨ ((𝜑 ∧ (𝜓 → (𝜃𝜂))) ∨ ((𝜓 → (𝜒𝜃)) ∧ (𝜓 → (𝜃𝜂))))) → (((𝜑𝜏) ∨ ((𝜓 → (𝜒𝜃)) ∧ 𝜏)) ∨ ((𝜑 ∧ (𝜓 → (𝜃𝜂))) ∨ (𝜓 → (𝜒𝜂)))))
159, 14ax-mp 7 . . . . . 6 (((𝜑𝜏) ∨ ((𝜓 → (𝜒𝜃)) ∧ 𝜏)) ∨ ((𝜑 ∧ (𝜓 → (𝜃𝜂))) ∨ (𝜓 → (𝜒𝜂))))
16 simpr 103 . . . . . . . 8 (((𝜑 ∨ (𝜓 → (𝜒𝜃))) ∧ 𝜏) → 𝜏)
176, 16sylbir 125 . . . . . . 7 (((𝜑𝜏) ∨ ((𝜓 → (𝜒𝜃)) ∧ 𝜏)) → 𝜏)
1817orim1i 677 . . . . . 6 ((((𝜑𝜏) ∨ ((𝜓 → (𝜒𝜃)) ∧ 𝜏)) ∨ ((𝜑 ∧ (𝜓 → (𝜃𝜂))) ∨ (𝜓 → (𝜒𝜂)))) → (𝜏 ∨ ((𝜑 ∧ (𝜓 → (𝜃𝜂))) ∨ (𝜓 → (𝜒𝜂)))))
1915, 18ax-mp 7 . . . . 5 (𝜏 ∨ ((𝜑 ∧ (𝜓 → (𝜃𝜂))) ∨ (𝜓 → (𝜒𝜂))))
20 simpl 102 . . . . . . 7 ((𝜑 ∧ (𝜓 → (𝜃𝜂))) → 𝜑)
2120orim1i 677 . . . . . 6 (((𝜑 ∧ (𝜓 → (𝜃𝜂))) ∨ (𝜓 → (𝜒𝜂))) → (𝜑 ∨ (𝜓 → (𝜒𝜂))))
2221orim2i 678 . . . . 5 ((𝜏 ∨ ((𝜑 ∧ (𝜓 → (𝜃𝜂))) ∨ (𝜓 → (𝜒𝜂)))) → (𝜏 ∨ (𝜑 ∨ (𝜓 → (𝜒𝜂)))))
2319, 22ax-mp 7 . . . 4 (𝜏 ∨ (𝜑 ∨ (𝜓 → (𝜒𝜂))))
24 orass 684 . . . 4 (((𝜏𝜑) ∨ (𝜓 → (𝜒𝜂))) ↔ (𝜏 ∨ (𝜑 ∨ (𝜓 → (𝜒𝜂)))))
2523, 24mpbir 134 . . 3 ((𝜏𝜑) ∨ (𝜓 → (𝜒𝜂)))
26 orcom 647 . . . 4 ((𝜏𝜑) ↔ (𝜑𝜏))
2726orbi1i 680 . . 3 (((𝜏𝜑) ∨ (𝜓 → (𝜒𝜂))) ↔ ((𝜑𝜏) ∨ (𝜓 → (𝜒𝜂))))
2825, 27mpbi 133 . 2 ((𝜑𝜏) ∨ (𝜓 → (𝜒𝜂)))
29 orass 684 . 2 (((𝜑𝜏) ∨ (𝜓 → (𝜒𝜂))) ↔ (𝜑 ∨ (𝜏 ∨ (𝜓 → (𝜒𝜂)))))
3028, 29mpbi 133 1 (𝜑 ∨ (𝜏 ∨ (𝜓 → (𝜒𝜂))))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97  wo 629
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  sbequi  1720
  Copyright terms: Public domain W3C validator