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 44522
Description: e222 44656 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 406 . . 3 ((𝜑𝜓) → 𝜒)
3 ee222.2 . . . 4 (𝜑 → (𝜓𝜃))
43imp 406 . . 3 ((𝜑𝜓) → 𝜃)
5 ee222.3 . . . 4 (𝜑 → (𝜓𝜏))
65imp 406 . . 3 ((𝜑𝜓) → 𝜏)
7 ee222.4 . . 3 (𝜒 → (𝜃 → (𝜏𝜂)))
82, 4, 6, 7syl3c 66 . 2 ((𝜑𝜓) → 𝜂)
98ex 412 1 (𝜑 → (𝜓𝜂))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  ee121  44525  ee122  44526  tratrb  44556  ee220  44658  ee202  44660  ee022  44662  ee002  44664  ee020  44666  ee200  44668  ee221  44670  ee212  44672  ee112  44675  ee211  44678  ee210  44680  ee201  44682  ee120  44684  ee021  44686  ee012  44688  ee102  44690  suctrALT2  44857
  Copyright terms: Public domain W3C validator