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

Theorem sbequilem 1766
Description: Propositional logic lemma used in the sbequi 1767 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 266 . . . . . . . . 9 ((𝜑 ∨ (𝜓 → (𝜒𝜃))) ∧ (𝜏 ∨ (𝜓 → (𝜃𝜂))))
4 andi 767 . . . . . . . . 9 (((𝜑 ∨ (𝜓 → (𝜒𝜃))) ∧ (𝜏 ∨ (𝜓 → (𝜃𝜂)))) ↔ (((𝜑 ∨ (𝜓 → (𝜒𝜃))) ∧ 𝜏) ∨ ((𝜑 ∨ (𝜓 → (𝜒𝜃))) ∧ (𝜓 → (𝜃𝜂)))))
53, 4mpbi 143 . . . . . . . 8 (((𝜑 ∨ (𝜓 → (𝜒𝜃))) ∧ 𝜏) ∨ ((𝜑 ∨ (𝜓 → (𝜒𝜃))) ∧ (𝜓 → (𝜃𝜂))))
6 andir 768 . . . . . . . . 9 (((𝜑 ∨ (𝜓 → (𝜒𝜃))) ∧ 𝜏) ↔ ((𝜑𝜏) ∨ ((𝜓 → (𝜒𝜃)) ∧ 𝜏)))
7 andir 768 . . . . . . . . 9 (((𝜑 ∨ (𝜓 → (𝜒𝜃))) ∧ (𝜓 → (𝜃𝜂))) ↔ ((𝜑 ∧ (𝜓 → (𝜃𝜂))) ∨ ((𝜓 → (𝜒𝜃)) ∧ (𝜓 → (𝜃𝜂)))))
86, 7orbi12i 716 . . . . . . . 8 ((((𝜑 ∨ (𝜓 → (𝜒𝜃))) ∧ 𝜏) ∨ ((𝜑 ∨ (𝜓 → (𝜒𝜃))) ∧ (𝜓 → (𝜃𝜂)))) ↔ (((𝜑𝜏) ∨ ((𝜓 → (𝜒𝜃)) ∧ 𝜏)) ∨ ((𝜑 ∧ (𝜓 → (𝜃𝜂))) ∨ ((𝜓 → (𝜒𝜃)) ∧ (𝜓 → (𝜃𝜂))))))
95, 8mpbi 143 . . . . . . 7 (((𝜑𝜏) ∨ ((𝜓 → (𝜒𝜃)) ∧ 𝜏)) ∨ ((𝜑 ∧ (𝜓 → (𝜃𝜂))) ∨ ((𝜓 → (𝜒𝜃)) ∧ (𝜓 → (𝜃𝜂)))))
10 pm3.43 569 . . . . . . . . . 10 (((𝜓 → (𝜒𝜃)) ∧ (𝜓 → (𝜃𝜂))) → (𝜓 → ((𝜒𝜃) ∧ (𝜃𝜂))))
11 pm3.33 337 . . . . . . . . . 10 (((𝜒𝜃) ∧ (𝜃𝜂)) → (𝜒𝜂))
1210, 11syl6 33 . . . . . . . . 9 (((𝜓 → (𝜒𝜃)) ∧ (𝜓 → (𝜃𝜂))) → (𝜓 → (𝜒𝜂)))
1312orim2i 713 . . . . . . . 8 (((𝜑 ∧ (𝜓 → (𝜃𝜂))) ∨ ((𝜓 → (𝜒𝜃)) ∧ (𝜓 → (𝜃𝜂)))) → ((𝜑 ∧ (𝜓 → (𝜃𝜂))) ∨ (𝜓 → (𝜒𝜂))))
1413orim2i 713 . . . . . . 7 ((((𝜑𝜏) ∨ ((𝜓 → (𝜒𝜃)) ∧ 𝜏)) ∨ ((𝜑 ∧ (𝜓 → (𝜃𝜂))) ∨ ((𝜓 → (𝜒𝜃)) ∧ (𝜓 → (𝜃𝜂))))) → (((𝜑𝜏) ∨ ((𝜓 → (𝜒𝜃)) ∧ 𝜏)) ∨ ((𝜑 ∧ (𝜓 → (𝜃𝜂))) ∨ (𝜓 → (𝜒𝜂)))))
159, 14ax-mp 7 . . . . . 6 (((𝜑𝜏) ∨ ((𝜓 → (𝜒𝜃)) ∧ 𝜏)) ∨ ((𝜑 ∧ (𝜓 → (𝜃𝜂))) ∨ (𝜓 → (𝜒𝜂))))
16 simpr 108 . . . . . . . 8 (((𝜑 ∨ (𝜓 → (𝜒𝜃))) ∧ 𝜏) → 𝜏)
176, 16sylbir 133 . . . . . . 7 (((𝜑𝜏) ∨ ((𝜓 → (𝜒𝜃)) ∧ 𝜏)) → 𝜏)
1817orim1i 712 . . . . . 6 ((((𝜑𝜏) ∨ ((𝜓 → (𝜒𝜃)) ∧ 𝜏)) ∨ ((𝜑 ∧ (𝜓 → (𝜃𝜂))) ∨ (𝜓 → (𝜒𝜂)))) → (𝜏 ∨ ((𝜑 ∧ (𝜓 → (𝜃𝜂))) ∨ (𝜓 → (𝜒𝜂)))))
1915, 18ax-mp 7 . . . . 5 (𝜏 ∨ ((𝜑 ∧ (𝜓 → (𝜃𝜂))) ∨ (𝜓 → (𝜒𝜂))))
20 simpl 107 . . . . . . 7 ((𝜑 ∧ (𝜓 → (𝜃𝜂))) → 𝜑)
2120orim1i 712 . . . . . 6 (((𝜑 ∧ (𝜓 → (𝜃𝜂))) ∨ (𝜓 → (𝜒𝜂))) → (𝜑 ∨ (𝜓 → (𝜒𝜂))))
2221orim2i 713 . . . . 5 ((𝜏 ∨ ((𝜑 ∧ (𝜓 → (𝜃𝜂))) ∨ (𝜓 → (𝜒𝜂)))) → (𝜏 ∨ (𝜑 ∨ (𝜓 → (𝜒𝜂)))))
2319, 22ax-mp 7 . . . 4 (𝜏 ∨ (𝜑 ∨ (𝜓 → (𝜒𝜂))))
24 orass 719 . . . 4 (((𝜏𝜑) ∨ (𝜓 → (𝜒𝜂))) ↔ (𝜏 ∨ (𝜑 ∨ (𝜓 → (𝜒𝜂)))))
2523, 24mpbir 144 . . 3 ((𝜏𝜑) ∨ (𝜓 → (𝜒𝜂)))
26 orcom 682 . . . 4 ((𝜏𝜑) ↔ (𝜑𝜏))
2726orbi1i 715 . . 3 (((𝜏𝜑) ∨ (𝜓 → (𝜒𝜂))) ↔ ((𝜑𝜏) ∨ (𝜓 → (𝜒𝜂))))
2825, 27mpbi 143 . 2 ((𝜑𝜏) ∨ (𝜓 → (𝜒𝜂)))
29 orass 719 . 2 (((𝜑𝜏) ∨ (𝜓 → (𝜒𝜂))) ↔ (𝜑 ∨ (𝜏 ∨ (𝜓 → (𝜒𝜂)))))
3028, 29mpbi 143 1 (𝜑 ∨ (𝜏 ∨ (𝜓 → (𝜒𝜂))))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wo 664
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  sbequi  1767
  Copyright terms: Public domain W3C validator