Mathbox for Alan Sare < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ee223 Structured version   Visualization version   GIF version

Theorem ee223 39176
 Description: e223 39177 without virtual deductions. (Contributed by Alan Sare, 12-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
ee223.1 (𝜑 → (𝜓𝜒))
ee223.2 (𝜑 → (𝜓𝜃))
ee223.3 (𝜑 → (𝜓 → (𝜏𝜂)))
ee223.4 (𝜒 → (𝜃 → (𝜂𝜁)))
Assertion
Ref Expression
ee223 (𝜑 → (𝜓 → (𝜏𝜁)))

Proof of Theorem ee223
StepHypRef Expression
1 ee223.2 . 2 (𝜑 → (𝜓𝜃))
2 ee223.3 . . . . . . . 8 (𝜑 → (𝜓 → (𝜏𝜂)))
3 ee223.1 . . . . . . . . . . . 12 (𝜑 → (𝜓𝜒))
4 ee223.4 . . . . . . . . . . . 12 (𝜒 → (𝜃 → (𝜂𝜁)))
53, 4syl6 35 . . . . . . . . . . 11 (𝜑 → (𝜓 → (𝜃 → (𝜂𝜁))))
65com34 91 . . . . . . . . . 10 (𝜑 → (𝜓 → (𝜂 → (𝜃𝜁))))
76com23 86 . . . . . . . . 9 (𝜑 → (𝜂 → (𝜓 → (𝜃𝜁))))
87com12 32 . . . . . . . 8 (𝜂 → (𝜑 → (𝜓 → (𝜃𝜁))))
92, 8syl8 76 . . . . . . 7 (𝜑 → (𝜓 → (𝜏 → (𝜑 → (𝜓 → (𝜃𝜁))))))
109com34 91 . . . . . 6 (𝜑 → (𝜓 → (𝜑 → (𝜏 → (𝜓 → (𝜃𝜁))))))
1110pm2.43a 54 . . . . 5 (𝜑 → (𝜓 → (𝜏 → (𝜓 → (𝜃𝜁)))))
1211com34 91 . . . 4 (𝜑 → (𝜓 → (𝜓 → (𝜏 → (𝜃𝜁)))))
1312pm2.43d 53 . . 3 (𝜑 → (𝜓 → (𝜏 → (𝜃𝜁))))
1413com34 91 . 2 (𝜑 → (𝜓 → (𝜃 → (𝜏𝜁))))
151, 14mpdd 43 1 (𝜑 → (𝜓 → (𝜏𝜁)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7 This theorem is referenced by:  e223  39177
 Copyright terms: Public domain W3C validator