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

Theorem e11 28460
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 28446 1  |-  (. ph  ->.  th
).
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd1 28337
This theorem is referenced by:  e11an  28461  e01  28463  e10  28467  elex2VD  28614  elex22VD  28615  eqsbc3rVD  28616  tpid3gVD  28618  3ornot23VD  28623  orbi1rVD  28624  3orbi123VD  28626  sbc3orgVD  28627  sbcoreleleqVD  28635  ordelordALTVD  28643  sbcim2gVD  28651  trsbcVD  28653  undif3VD  28658  sbcssVD  28659  csbingVD  28660  onfrALTVD  28667  csbeq2gVD  28668  csbsngVD  28669  csbxpgVD  28670  csbresgVD  28671  csbrngVD  28672  csbima12gALTVD  28673  csbunigVD  28674  csbfv12gALTVD  28675  19.41rgVD  28678  2pm13.193VD  28679  hbimpgVD  28680  a9e2eqVD  28683  2uasbanhVD  28687  notnot2ALTVD  28691
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 28338
  Copyright terms: Public domain W3C validator