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

Theorem e11 28765
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 10 . 2  |-  ( ps 
->  ( ps  ->  ( ch  ->  th ) ) )
51, 1, 2, 4e111 28751 1  |-  (. ph  ->.  th
).
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd1 28636
This theorem is referenced by:  e11an  28766  e01  28768  e10  28772  elex2VD  28930  elex22VD  28931  eqsbc3rVD  28932  tpid3gVD  28934  3ornot23VD  28939  orbi1rVD  28940  3orbi123VD  28942  sbc3orgVD  28943  sbcoreleleqVD  28951  ordelordALTVD  28959  sbcim2gVD  28967  trsbcVD  28969  undif3VD  28974  sbcssVD  28975  csbingVD  28976  onfrALTVD  28983  csbeq2gVD  28984  csbsngVD  28985  csbxpgVD  28986  csbresgVD  28987  csbrngVD  28988  csbima12gALTVD  28989  csbunigVD  28990  csbfv12gALTVD  28991  19.41rgVD  28994  2pm13.193VD  28995  hbimpgVD  28996  a9e2eqVD  28999  2uasbanhVD  29003  notnot2ALTVD  29007
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-vd1 28637
  Copyright terms: Public domain W3C validator