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 43422
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 43387 1 (   𝜑   ,   𝜓   ▶   𝜏   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd2 43328
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 206  df-an 397  df-vd2 43329
This theorem is referenced by:  e22an  43423  e02  43448  e12  43475  e20  43478  e21  43481  sspwtr  43572  pwtrVD  43575  pwtrrVD  43576  elex22VD  43590  tpid3gVD  43593  en3lplem2VD  43595  imbi12VD  43624  truniALTVD  43629  trintALTVD  43631  onfrALTlem3VD  43638  onfrALTlem2VD  43640  ax6e2eqVD  43658  ax6e2ndeqVD  43660  sb5ALTVD  43664
  Copyright terms: Public domain W3C validator