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

Theorem ee222 42876
Description: e222 43010 without virtual deduction connectives. Special theorem needed for the Virtual Deduction translation tool. (Contributed by Alan Sare, 7-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
ee222.1 (𝜑 → (𝜓𝜒))
ee222.2 (𝜑 → (𝜓𝜃))
ee222.3 (𝜑 → (𝜓𝜏))
ee222.4 (𝜒 → (𝜃 → (𝜏𝜂)))
Assertion
Ref Expression
ee222 (𝜑 → (𝜓𝜂))

Proof of Theorem ee222
StepHypRef Expression
1 ee222.1 . . . 4 (𝜑 → (𝜓𝜒))
21imp 408 . . 3 ((𝜑𝜓) → 𝜒)
3 ee222.2 . . . 4 (𝜑 → (𝜓𝜃))
43imp 408 . . 3 ((𝜑𝜓) → 𝜃)
5 ee222.3 . . . 4 (𝜑 → (𝜓𝜏))
65imp 408 . . 3 ((𝜑𝜓) → 𝜏)
7 ee222.4 . . 3 (𝜒 → (𝜃 → (𝜏𝜂)))
82, 4, 6, 7syl3c 66 . 2 ((𝜑𝜓) → 𝜂)
98ex 414 1 (𝜑 → (𝜓𝜂))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 206  df-an 398
This theorem is referenced by:  ee121  42879  ee122  42880  tratrb  42910  ee220  43012  ee202  43014  ee022  43016  ee002  43018  ee020  43020  ee200  43022  ee221  43024  ee212  43026  ee112  43029  ee211  43032  ee210  43034  ee201  43036  ee120  43038  ee021  43040  ee012  43042  ee102  43044  suctrALT2  43211
  Copyright terms: Public domain W3C validator