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

Theorem sbequilem 1811
Description: Propositional logic lemma used in the sbequi 1812 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  1812
  Copyright terms: Public domain W3C validator