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 41188
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 41153 1 (   𝜑   ,   𝜓   ▶   𝜏   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd2 41094
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  df-vd2 41095
This theorem is referenced by:  e22an  41189  e02  41214  e12  41241  e20  41244  e21  41247  sspwtr  41338  pwtrVD  41341  pwtrrVD  41342  elex22VD  41356  tpid3gVD  41359  en3lplem2VD  41361  imbi12VD  41390  truniALTVD  41395  trintALTVD  41397  onfrALTlem3VD  41404  onfrALTlem2VD  41406  ax6e2eqVD  41424  ax6e2ndeqVD  41426  sb5ALTVD  41430
  Copyright terms: Public domain W3C validator