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

Theorem e11 36704
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 36690 1  |-  (. ph  ->.  th
).
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd1 36576
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 188  df-vd1 36577
This theorem is referenced by:  e11an  36705  e01  36707  e10  36710  elex2VD  36873  elex22VD  36874  eqsbc3rVD  36875  tpid3gVD  36877  3ornot23VD  36882  orbi1rVD  36883  3orbi123VD  36885  sbc3orgVD  36886  sbcoreleleqVD  36895  ordelordALTVD  36903  sbcim2gVD  36911  trsbcVD  36913  undif3VD  36918  sbcssgVD  36919  csbingVD  36920  onfrALTVD  36927  csbeq2gVD  36928  csbsngVD  36929  csbxpgVD  36930  csbresgVD  36931  csbrngVD  36932  csbima12gALTVD  36933  csbunigVD  36934  csbfv12gALTVD  36935  19.41rgVD  36938  2pm13.193VD  36939  hbimpgVD  36940  ax6e2eqVD  36943  2uasbanhVD  36947  notnot2ALTVD  36951
  Copyright terms: Public domain W3C validator