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

Theorem e22 44696
Description: A virtual deduction elimination rule. (Contributed by Alan Sare, 2-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
e22.1 (   𝜑   ,   𝜓   ▶   𝜒   )
e22.2 (   𝜑   ,   𝜓   ▶   𝜃   )
e22.3 (𝜒 → (𝜃𝜏))
Assertion
Ref Expression
e22 (   𝜑   ,   𝜓   ▶   𝜏   )

Proof of Theorem e22
StepHypRef Expression
1 e22.1 . 2 (   𝜑   ,   𝜓   ▶   𝜒   )
2 e22.2 . 2 (   𝜑   ,   𝜓   ▶   𝜃   )
3 e22.3 . . 3 (𝜒 → (𝜃𝜏))
43a1i 11 . 2 (𝜒 → (𝜒 → (𝜃𝜏)))
51, 1, 2, 4e222 44661 1 (   𝜑   ,   𝜓   ▶   𝜏   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd2 44602
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  df-vd2 44603
This theorem is referenced by:  e22an  44697  e02  44722  e12  44749  e20  44752  e21  44755  sspwtr  44846  pwtrVD  44849  pwtrrVD  44850  elex22VD  44864  tpid3gVD  44867  en3lplem2VD  44869  imbi12VD  44898  truniALTVD  44903  trintALTVD  44905  onfrALTlem3VD  44912  onfrALTlem2VD  44914  ax6e2eqVD  44932  ax6e2ndeqVD  44934  sb5ALTVD  44938
  Copyright terms: Public domain W3C validator