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

Theorem e11 33617
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  |-  (. ph  ->.  ps
).
e11.2  |-  (. ph  ->.  ch
).
e11.3  |-  ( ps 
->  ( ch  ->  th )
)
Assertion
Ref Expression
e11  |-  (. ph  ->.  th
).

Proof of Theorem e11
StepHypRef Expression
1 e11.1 . 2  |-  (. ph  ->.  ps
).
2 e11.2 . 2  |-  (. ph  ->.  ch
).
3 e11.3 . . 3  |-  ( ps 
->  ( ch  ->  th )
)
43a1i 11 . 2  |-  ( ps 
->  ( ps  ->  ( ch  ->  th ) ) )
51, 1, 2, 4e111 33603 1  |-  (. ph  ->.  th
).
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd1 33489
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 185  df-vd1 33490
This theorem is referenced by:  e11an  33618  e01  33620  e10  33623  elex2VD  33781  elex22VD  33782  eqsbc3rVD  33783  tpid3gVD  33785  3ornot23VD  33790  orbi1rVD  33791  3orbi123VD  33793  sbc3orgVD  33794  sbcoreleleqVD  33802  ordelordALTVD  33810  sbcim2gVD  33818  trsbcVD  33820  undif3VD  33825  sbcssgVD  33826  csbingVD  33827  onfrALTVD  33834  csbeq2gVD  33835  csbsngVD  33836  csbxpgVD  33837  csbresgVD  33838  csbrngVD  33839  csbima12gALTVD  33840  csbunigVD  33841  csbfv12gALTVD  33842  19.41rgVD  33845  2pm13.193VD  33846  hbimpgVD  33847  ax6e2eqVD  33850  2uasbanhVD  33854  notnot2ALTVD  33858
  Copyright terms: Public domain W3C validator