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

Theorem e11 28790
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 28776 1  |-  (. ph  ->.  th
).
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd1 28661
This theorem is referenced by:  e11an  28791  e01  28793  e10  28796  elex2VD  28951  elex22VD  28952  eqsbc3rVD  28953  tpid3gVD  28955  3ornot23VD  28960  orbi1rVD  28961  3orbi123VD  28963  sbc3orgVD  28964  sbcoreleleqVD  28972  ordelordALTVD  28980  sbcim2gVD  28988  trsbcVD  28990  undif3VD  28995  sbcssVD  28996  csbingVD  28997  onfrALTVD  29004  csbeq2gVD  29005  csbsngVD  29006  csbxpgVD  29007  csbresgVD  29008  csbrngVD  29009  csbima12gALTVD  29010  csbunigVD  29011  csbfv12gALTVD  29012  19.41rgVD  29015  2pm13.193VD  29016  hbimpgVD  29017  a9e2eqVD  29020  2uasbanhVD  29024  notnot2ALTVD  29028
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 179  df-vd1 28662
  Copyright terms: Public domain W3C validator