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 39025
Description: e222 39178 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 444 . . 3 ((𝜑𝜓) → 𝜒)
3 ee222.2 . . . 4 (𝜑 → (𝜓𝜃))
43imp 444 . . 3 ((𝜑𝜓) → 𝜃)
5 ee222.3 . . . 4 (𝜑 → (𝜓𝜏))
65imp 444 . . 3 ((𝜑𝜓) → 𝜏)
7 ee222.4 . . 3 (𝜒 → (𝜃 → (𝜏𝜂)))
82, 4, 6, 7syl3c 66 . 2 ((𝜑𝜓) → 𝜂)
98ex 449 1 (𝜑 → (𝜓𝜂))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  ee121  39028  ee122  39029  tratrb  39063  ee220  39180  ee202  39182  ee022  39184  ee002  39186  ee020  39188  ee200  39190  ee221  39192  ee212  39194  ee112  39197  ee211  39200  ee210  39202  ee201  39204  ee120  39206  ee021  39208  ee012  39210  ee102  39212  suctrALT2  39386
  Copyright terms: Public domain W3C validator