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 40713
Description: e222 40847 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 407 . . 3 ((𝜑𝜓) → 𝜒)
3 ee222.2 . . . 4 (𝜑 → (𝜓𝜃))
43imp 407 . . 3 ((𝜑𝜓) → 𝜃)
5 ee222.3 . . . 4 (𝜑 → (𝜓𝜏))
65imp 407 . . 3 ((𝜑𝜓) → 𝜏)
7 ee222.4 . . 3 (𝜒 → (𝜃 → (𝜏𝜂)))
82, 4, 6, 7syl3c 66 . 2 ((𝜑𝜓) → 𝜂)
98ex 413 1 (𝜑 → (𝜓𝜂))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  ee121  40716  ee122  40717  tratrb  40747  ee220  40849  ee202  40851  ee022  40853  ee002  40855  ee020  40857  ee200  40859  ee221  40861  ee212  40863  ee112  40866  ee211  40869  ee210  40871  ee201  40873  ee120  40875  ee021  40877  ee012  40879  ee102  40881  suctrALT2  41048
  Copyright terms: Public domain W3C validator