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

Theorem e11 36975
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 36961 1  |-  (. ph  ->.  th
).
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd1 36847
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 36848
This theorem is referenced by:  e11an  36976  e01  36978  e10  36981  elex2VD  37144  elex22VD  37145  eqsbc3rVD  37146  tpid3gVD  37148  3ornot23VD  37153  orbi1rVD  37154  3orbi123VD  37156  sbc3orgVD  37157  sbcoreleleqVD  37166  ordelordALTVD  37174  sbcim2gVD  37182  trsbcVD  37184  undif3VD  37189  sbcssgVD  37190  csbingVD  37191  onfrALTVD  37198  csbeq2gVD  37199  csbsngVD  37200  csbxpgVD  37201  csbresgVD  37202  csbrngVD  37203  csbima12gALTVD  37204  csbunigVD  37205  csbfv12gALTVD  37206  19.41rgVD  37209  2pm13.193VD  37210  hbimpgVD  37211  ax6e2eqVD  37214  2uasbanhVD  37218  notnot2ALTVD  37222
  Copyright terms: Public domain W3C validator