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 44669
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 44634 1 (   𝜑   ,   𝜓   ▶   𝜏   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd2 44575
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 44576
This theorem is referenced by:  e22an  44670  e02  44695  e12  44722  e20  44725  e21  44728  sspwtr  44819  pwtrVD  44822  pwtrrVD  44823  elex22VD  44837  tpid3gVD  44840  en3lplem2VD  44842  imbi12VD  44871  truniALTVD  44876  trintALTVD  44878  onfrALTlem3VD  44885  onfrALTlem2VD  44887  ax6e2eqVD  44905  ax6e2ndeqVD  44907  sb5ALTVD  44911
  Copyright terms: Public domain W3C validator