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 39417
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 39382 1 (   𝜑   ,   𝜓   ▶   𝜏   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd2 39314
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  df-vd2 39315
This theorem is referenced by:  e22an  39418  e02  39443  e12  39472  e20  39475  e21  39478  sspwtr  39569  pwtrVD  39577  pwtrrVD  39578  elex22VD  39592  tpid3gVD  39595  en3lplem2VD  39597  imbi12VD  39627  truniALTVD  39632  trintALTVD  39634  onfrALTlem3VD  39641  onfrALTlem2VD  39643  ax6e2eqVD  39661  ax6e2ndeqVD  39663  sb5ALTVD  39667
  Copyright terms: Public domain W3C validator