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

Theorem ee12an 1353
Description: e12an 28814 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  2008  xpcan  5128  xpcan2  5129  mapxpen  7043  sucdom2  7073  f1finf1o  7102  unfi  7140  inf3lem3  7347  dfac12r  7788  cfsuc  7899  fin23lem26  7967  iundom2g  8178  inar1  8413  rankcf  8415  ltsrpr  8715  supsrlem  8749  axpre-sup  8807  infmrcl  9749  nominpos  9964  ublbneg  10318  qbtwnre  10542  fsequb  11053  rexanre  11846  rexuzre  11852  rexico  11853  caubnd  11858  rlim2lt  11987  rlim3  11988  lo1bddrp  12015  o1lo1  12027  climshftlem  12064  rlimcn2  12080  rlimo1  12106  lo1add  12116  lo1mul  12117  lo1le  12141  isercoll  12157  serf0  12169  cvgcmp  12290  dvds1lem  12556  dvds2lem  12557  isprm5  12807  vdwlem2  13045  vdwlem10  13053  vdwlem11  13054  lsmcv  15910  lmconst  17007  ptcnplem  17331  fclscmp  17741  tsmsres  17842  addcnlem  18384  lebnumlem3  18477  xlebnum  18479  lebnumii  18480  iscmet3lem2  18734  bcthlem4  18765  cniccbdd  18837  ovoliunlem2  18878  mbfi1flimlem  19093  ply1divex  19538  aalioulem3  19730  aalioulem5  19732  aalioulem6  19733  aaliou  19734  ulmshftlem  19784  ulmbdd  19791  tanarg  19986  cxploglim  20288  ftalem2  20327  ftalem7  20332  dchrisumlem3  20656  ubthlem3  21467  spansncol  22163  riesz1  22661  erdsze2lem2  23750  dfrdg4  24560  onsuct0  24952  neibastop2  26413  incsequz  26561  caushft  26580  cntotbnd  26623  expgrowth  27655  nvnencycllem  28389  vk15.4j  28590  sstrALT2  28927  dfsb2NEW7  29609  4atexlemex4  30884
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