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

Theorem e11 37109
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 37095 1  |-  (. ph  ->.  th
).
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd1 36981
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 190  df-vd1 36982
This theorem is referenced by:  e11an  37110  e01  37112  e10  37115  elex2VD  37273  elex22VD  37274  eqsbc3rVD  37275  tpid3gVD  37277  3ornot23VD  37282  orbi1rVD  37283  3orbi123VD  37285  sbc3orgVD  37286  sbcoreleleqVD  37295  ordelordALTVD  37303  sbcim2gVD  37311  trsbcVD  37313  undif3VD  37318  sbcssgVD  37319  csbingVD  37320  onfrALTVD  37327  csbeq2gVD  37328  csbsngVD  37329  csbxpgVD  37330  csbresgVD  37331  csbrngVD  37332  csbima12gALTVD  37333  csbunigVD  37334  csbfv12gALTVD  37335  19.41rgVD  37338  2pm13.193VD  37339  hbimpgVD  37340  ax6e2eqVD  37343  2uasbanhVD  37347  notnot2ALTVD  37351
  Copyright terms: Public domain W3C validator