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

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

Proof of Theorem e11
StepHypRef Expression
1 e11.1 . 2 (   𝜑   ▶   𝜓   )
2 e11.2 . 2 (   𝜑   ▶   𝜒   )
3 e11.3 . . 3 (𝜓 → (𝜒𝜃))
43a1i 11 . 2 (𝜓 → (𝜓 → (𝜒𝜃)))
51, 1, 2, 4e111 39216 1 (   𝜑   ▶   𝜃   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd1 39102
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-vd1 39103
This theorem is referenced by:  e11an  39231  e01  39233  e10  39236  elex2VD  39387  elex22VD  39388  eqsbc3rVD  39389  tpid3gVD  39391  3ornot23VD  39396  orbi1rVD  39397  3orbi123VD  39399  sbc3orgVD  39400  sbcoreleleqVD  39409  ordelordALTVD  39417  sbcim2gVD  39425  trsbcVD  39427  undif3VD  39432  sbcssgVD  39433  csbingVD  39434  onfrALTVD  39441  csbeq2gVD  39442  csbsngVD  39443  csbxpgVD  39444  csbresgVD  39445  csbrngVD  39446  csbima12gALTVD  39447  csbunigVD  39448  csbfv12gALTVD  39449  19.41rgVD  39452  2pm13.193VD  39453  hbimpgVD  39454  ax6e2eqVD  39457  2uasbanhVD  39461  notnotrALTVD  39465
  Copyright terms: Public domain W3C validator