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

Theorem ee12an 1373
Description: e12an 28839 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 529 . 2  |-  ( ph  ->  ( ch  ->  ( ps  /\  th ) ) )
4 ee12an.3 . 2  |-  ( ( ps  /\  th )  ->  ta )
53, 4syl6 32 1  |-  ( ph  ->  ( ch  ->  ta ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  dfsb2  2110  xpcan  5307  xpcan2  5308  mapxpen  7275  sucdom2  7305  f1finf1o  7337  unfi  7376  inf3lem3  7587  dfac12r  8028  cfsuc  8139  fin23lem26  8207  iundom2g  8417  inar1  8652  rankcf  8654  ltsrpr  8954  supsrlem  8988  axpre-sup  9046  infmrcl  9989  nominpos  10206  ublbneg  10562  qbtwnre  10787  fsequb  11316  brfi1uzind  11717  rexanre  12152  rexuzre  12158  rexico  12159  caubnd  12164  rlim2lt  12293  rlim3  12294  lo1bddrp  12321  o1lo1  12333  climshftlem  12370  rlimcn2  12386  rlimo1  12412  lo1add  12422  lo1mul  12423  lo1le  12447  isercoll  12463  serf0  12476  cvgcmp  12597  dvds1lem  12863  dvds2lem  12864  isprm5  13114  vdwlem2  13352  vdwlem10  13360  vdwlem11  13361  lsmcv  16215  lmconst  17327  ptcnplem  17655  fclscmp  18064  tsmsres  18175  addcnlem  18896  lebnumlem3  18990  xlebnum  18992  lebnumii  18993  iscmet3lem2  19247  bcthlem4  19282  cniccbdd  19360  ovoliunlem2  19401  mbfi1flimlem  19616  ply1divex  20061  aalioulem3  20253  aalioulem5  20255  aalioulem6  20256  aaliou  20257  ulmshftlem  20307  ulmbdd  20316  tanarg  20516  cxploglim  20818  ftalem2  20858  ftalem7  20863  dchrisumlem3  21187  nvnencycllem  21632  ubthlem3  22376  spansncol  23072  riesz1  23570  erdsze2lem2  24892  dfrdg4  25797  onsuct0  26193  neibastop2  26392  incsequz  26454  caushft  26469  equivbnd  26501  cntotbnd  26507  expgrowth  27531  vk15.4j  28614  sstrALT2  28949  dfsb2NEW7  29640  4atexlemex4  30872
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-an 362
  Copyright terms: Public domain W3C validator