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

Theorem sbequilem 1735
Description: Propositional logic lemma used in the sbequi 1736 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 261 . . . . . . . . 9 ((𝜑 ∨ (𝜓 → (𝜒𝜃))) ∧ (𝜏 ∨ (𝜓 → (𝜃𝜂))))
4 andi 742 . . . . . . . . 9 (((𝜑 ∨ (𝜓 → (𝜒𝜃))) ∧ (𝜏 ∨ (𝜓 → (𝜃𝜂)))) ↔ (((𝜑 ∨ (𝜓 → (𝜒𝜃))) ∧ 𝜏) ∨ ((𝜑 ∨ (𝜓 → (𝜒𝜃))) ∧ (𝜓 → (𝜃𝜂)))))
53, 4mpbi 137 . . . . . . . 8 (((𝜑 ∨ (𝜓 → (𝜒𝜃))) ∧ 𝜏) ∨ ((𝜑 ∨ (𝜓 → (𝜒𝜃))) ∧ (𝜓 → (𝜃𝜂))))
6 andir 743 . . . . . . . . 9 (((𝜑 ∨ (𝜓 → (𝜒𝜃))) ∧ 𝜏) ↔ ((𝜑𝜏) ∨ ((𝜓 → (𝜒𝜃)) ∧ 𝜏)))
7 andir 743 . . . . . . . . 9 (((𝜑 ∨ (𝜓 → (𝜒𝜃))) ∧ (𝜓 → (𝜃𝜂))) ↔ ((𝜑 ∧ (𝜓 → (𝜃𝜂))) ∨ ((𝜓 → (𝜒𝜃)) ∧ (𝜓 → (𝜃𝜂)))))
86, 7orbi12i 691 . . . . . . . 8 ((((𝜑 ∨ (𝜓 → (𝜒𝜃))) ∧ 𝜏) ∨ ((𝜑 ∨ (𝜓 → (𝜒𝜃))) ∧ (𝜓 → (𝜃𝜂)))) ↔ (((𝜑𝜏) ∨ ((𝜓 → (𝜒𝜃)) ∧ 𝜏)) ∨ ((𝜑 ∧ (𝜓 → (𝜃𝜂))) ∨ ((𝜓 → (𝜒𝜃)) ∧ (𝜓 → (𝜃𝜂))))))
95, 8mpbi 137 . . . . . . 7 (((𝜑𝜏) ∨ ((𝜓 → (𝜒𝜃)) ∧ 𝜏)) ∨ ((𝜑 ∧ (𝜓 → (𝜃𝜂))) ∨ ((𝜓 → (𝜒𝜃)) ∧ (𝜓 → (𝜃𝜂)))))
10 pm3.43 544 . . . . . . . . . 10 (((𝜓 → (𝜒𝜃)) ∧ (𝜓 → (𝜃𝜂))) → (𝜓 → ((𝜒𝜃) ∧ (𝜃𝜂))))
11 pm3.33 331 . . . . . . . . . 10 (((𝜒𝜃) ∧ (𝜃𝜂)) → (𝜒𝜂))
1210, 11syl6 33 . . . . . . . . 9 (((𝜓 → (𝜒𝜃)) ∧ (𝜓 → (𝜃𝜂))) → (𝜓 → (𝜒𝜂)))
1312orim2i 688 . . . . . . . 8 (((𝜑 ∧ (𝜓 → (𝜃𝜂))) ∨ ((𝜓 → (𝜒𝜃)) ∧ (𝜓 → (𝜃𝜂)))) → ((𝜑 ∧ (𝜓 → (𝜃𝜂))) ∨ (𝜓 → (𝜒𝜂))))
1413orim2i 688 . . . . . . 7 ((((𝜑𝜏) ∨ ((𝜓 → (𝜒𝜃)) ∧ 𝜏)) ∨ ((𝜑 ∧ (𝜓 → (𝜃𝜂))) ∨ ((𝜓 → (𝜒𝜃)) ∧ (𝜓 → (𝜃𝜂))))) → (((𝜑𝜏) ∨ ((𝜓 → (𝜒𝜃)) ∧ 𝜏)) ∨ ((𝜑 ∧ (𝜓 → (𝜃𝜂))) ∨ (𝜓 → (𝜒𝜂)))))
159, 14ax-mp 7 . . . . . 6 (((𝜑𝜏) ∨ ((𝜓 → (𝜒𝜃)) ∧ 𝜏)) ∨ ((𝜑 ∧ (𝜓 → (𝜃𝜂))) ∨ (𝜓 → (𝜒𝜂))))
16 simpr 107 . . . . . . . 8 (((𝜑 ∨ (𝜓 → (𝜒𝜃))) ∧ 𝜏) → 𝜏)
176, 16sylbir 129 . . . . . . 7 (((𝜑𝜏) ∨ ((𝜓 → (𝜒𝜃)) ∧ 𝜏)) → 𝜏)
1817orim1i 687 . . . . . 6 ((((𝜑𝜏) ∨ ((𝜓 → (𝜒𝜃)) ∧ 𝜏)) ∨ ((𝜑 ∧ (𝜓 → (𝜃𝜂))) ∨ (𝜓 → (𝜒𝜂)))) → (𝜏 ∨ ((𝜑 ∧ (𝜓 → (𝜃𝜂))) ∨ (𝜓 → (𝜒𝜂)))))
1915, 18ax-mp 7 . . . . 5 (𝜏 ∨ ((𝜑 ∧ (𝜓 → (𝜃𝜂))) ∨ (𝜓 → (𝜒𝜂))))
20 simpl 106 . . . . . . 7 ((𝜑 ∧ (𝜓 → (𝜃𝜂))) → 𝜑)
2120orim1i 687 . . . . . 6 (((𝜑 ∧ (𝜓 → (𝜃𝜂))) ∨ (𝜓 → (𝜒𝜂))) → (𝜑 ∨ (𝜓 → (𝜒𝜂))))
2221orim2i 688 . . . . 5 ((𝜏 ∨ ((𝜑 ∧ (𝜓 → (𝜃𝜂))) ∨ (𝜓 → (𝜒𝜂)))) → (𝜏 ∨ (𝜑 ∨ (𝜓 → (𝜒𝜂)))))
2319, 22ax-mp 7 . . . 4 (𝜏 ∨ (𝜑 ∨ (𝜓 → (𝜒𝜂))))
24 orass 694 . . . 4 (((𝜏𝜑) ∨ (𝜓 → (𝜒𝜂))) ↔ (𝜏 ∨ (𝜑 ∨ (𝜓 → (𝜒𝜂)))))
2523, 24mpbir 138 . . 3 ((𝜏𝜑) ∨ (𝜓 → (𝜒𝜂)))
26 orcom 657 . . . 4 ((𝜏𝜑) ↔ (𝜑𝜏))
2726orbi1i 690 . . 3 (((𝜏𝜑) ∨ (𝜓 → (𝜒𝜂))) ↔ ((𝜑𝜏) ∨ (𝜓 → (𝜒𝜂))))
2825, 27mpbi 137 . 2 ((𝜑𝜏) ∨ (𝜓 → (𝜒𝜂)))
29 orass 694 . 2 (((𝜑𝜏) ∨ (𝜓 → (𝜒𝜂))) ↔ (𝜑 ∨ (𝜏 ∨ (𝜓 → (𝜒𝜂)))))
3028, 29mpbi 137 1 (𝜑 ∨ (𝜏 ∨ (𝜓 → (𝜒𝜂))))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  wo 639
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  sbequi  1736
  Copyright terms: Public domain W3C validator