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 43434
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 43420 1 (   𝜑   ▶   𝜃   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd1 43315
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-vd1 43316
This theorem is referenced by:  e11an  43435  e01  43437  e10  43440  elex2VD  43584  elex22VD  43585  eqsbc2VD  43586  tpid3gVD  43588  3ornot23VD  43593  orbi1rVD  43594  3orbi123VD  43596  sbc3orgVD  43597  ordelordALTVD  43613  sbcim2gVD  43621  trsbcVD  43623  undif3VD  43628  sbcssgVD  43629  csbingVD  43630  onfrALTVD  43637  csbeq2gVD  43638  csbsngVD  43639  csbxpgVD  43640  csbresgVD  43641  csbrngVD  43642  csbima12gALTVD  43643  csbunigVD  43644  csbfv12gALTVD  43645  19.41rgVD  43648  2pm13.193VD  43649  hbimpgVD  43650  ax6e2eqVD  43653  2uasbanhVD  43657  notnotrALTVD  43661
  Copyright terms: Public domain W3C validator