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 41205
Description: e222 41339 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 410 . . 3 ((𝜑𝜓) → 𝜒)
3 ee222.2 . . . 4 (𝜑 → (𝜓𝜃))
43imp 410 . . 3 ((𝜑𝜓) → 𝜃)
5 ee222.3 . . . 4 (𝜑 → (𝜓𝜏))
65imp 410 . . 3 ((𝜑𝜓) → 𝜏)
7 ee222.4 . . 3 (𝜒 → (𝜃 → (𝜏𝜂)))
82, 4, 6, 7syl3c 66 . 2 ((𝜑𝜓) → 𝜂)
98ex 416 1 (𝜑 → (𝜓𝜂))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  ee121  41208  ee122  41209  tratrb  41239  ee220  41341  ee202  41343  ee022  41345  ee002  41347  ee020  41349  ee200  41351  ee221  41353  ee212  41355  ee112  41358  ee211  41361  ee210  41363  ee201  41365  ee120  41367  ee021  41369  ee012  41371  ee102  41373  suctrALT2  41540
  Copyright terms: Public domain W3C validator