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

Theorem e11 32771
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 32757 1  |-  (. ph  ->.  th
).
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd1 32643
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 185  df-vd1 32644
This theorem is referenced by:  e11an  32772  e01  32774  e10  32777  elex2VD  32935  elex22VD  32936  eqsbc3rVD  32937  tpid3gVD  32939  3ornot23VD  32944  orbi1rVD  32945  3orbi123VD  32947  sbc3orgVD  32948  sbcoreleleqVD  32956  ordelordALTVD  32964  sbcim2gVD  32972  trsbcVD  32974  undif3VD  32979  sbcssgVD  32980  csbingVD  32981  onfrALTVD  32988  csbeq2gVD  32989  csbsngVD  32990  csbxpgVD  32991  csbresgVD  32992  csbrngVD  32993  csbima12gALTVD  32994  csbunigVD  32995  csbfv12gALTVD  32996  19.41rgVD  32999  2pm13.193VD  33000  hbimpgVD  33001  ax6e2eqVD  33004  2uasbanhVD  33008  notnot2ALTVD  33012
  Copyright terms: Public domain W3C validator