MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ee12an Unicode version

Theorem ee12an 1353
Description: e12an 28500 without virtual deduction connectives. Special theorem needed for Alan Sare's virtual deduction translation tool. (Contributed by Alan Sare, 28-Oct-2011.) TODO: this is frequently used; come up with better label.
Hypotheses
Ref Expression
ee12an.1  |-  ( ph  ->  ps )
ee12an.2  |-  ( ph  ->  ( ch  ->  th )
)
ee12an.3  |-  ( ( ps  /\  th )  ->  ta )
Assertion
Ref Expression
ee12an  |-  ( ph  ->  ( ch  ->  ta ) )

Proof of Theorem ee12an
StepHypRef Expression
1 ee12an.2 . . 3  |-  ( ph  ->  ( ch  ->  th )
)
2 ee12an.1 . . 3  |-  ( ph  ->  ps )
31, 2jctild 527 . 2  |-  ( ph  ->  ( ch  ->  ( ps  /\  th ) ) )
4 ee12an.3 . 2  |-  ( ( ps  /\  th )  ->  ta )
53, 4syl6 29 1  |-  ( ph  ->  ( ch  ->  ta ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  dfsb2  1995  xpcan  5112  xpcan2  5113  mapxpen  7027  sucdom2  7057  f1finf1o  7086  unfi  7124  inf3lem3  7331  dfac12r  7772  cfsuc  7883  fin23lem26  7951  iundom2g  8162  inar1  8397  rankcf  8399  ltsrpr  8699  supsrlem  8733  axpre-sup  8791  infmrcl  9733  nominpos  9948  ublbneg  10302  qbtwnre  10526  fsequb  11037  rexanre  11830  rexuzre  11836  rexico  11837  caubnd  11842  rlim2lt  11971  rlim3  11972  lo1bddrp  11999  o1lo1  12011  climshftlem  12048  rlimcn2  12064  rlimo1  12090  lo1add  12100  lo1mul  12101  lo1le  12125  isercoll  12141  serf0  12153  cvgcmp  12274  dvds1lem  12540  dvds2lem  12541  isprm5  12791  vdwlem2  13029  vdwlem10  13037  vdwlem11  13038  lsmcv  15894  lmconst  16991  ptcnplem  17315  fclscmp  17725  tsmsres  17826  addcnlem  18368  lebnumlem3  18461  xlebnum  18463  lebnumii  18464  iscmet3lem2  18718  bcthlem4  18749  cniccbdd  18821  ovoliunlem2  18862  mbfi1flimlem  19077  ply1divex  19522  aalioulem3  19714  aalioulem5  19716  aalioulem6  19717  aaliou  19718  ulmshftlem  19768  ulmbdd  19775  tanarg  19970  cxploglim  20272  ftalem2  20311  ftalem7  20316  dchrisumlem3  20640  ubthlem3  21451  spansncol  22147  riesz1  22645  erdsze2lem2  23735  dfrdg4  24488  onsuct0  24880  neibastop2  26310  incsequz  26458  caushft  26477  cntotbnd  26520  expgrowth  27552  vk15.4j  28291  sstrALT2  28611  4atexlemex4  30262
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-an 360
  Copyright terms: Public domain W3C validator