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

Theorem exp4a 589
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
exp4a.1  |-  ( ph  ->  ( ps  ->  (
( ch  /\  th )  ->  ta ) ) )
Assertion
Ref Expression
exp4a  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )

Proof of Theorem exp4a
StepHypRef Expression
1 exp4a.1 . 2  |-  ( ph  ->  ( ps  ->  (
( ch  /\  th )  ->  ta ) ) )
2 impexp 433 . 2  |-  ( ( ( ch  /\  th )  ->  ta )  <->  ( ch  ->  ( th  ->  ta ) ) )
31, 2syl6ib 217 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  exp4b  590  exp4d  592  exp45  597  exp5c  599  tz7.7  4418  riotasv2dOLD  6350  tfr3  6415  oaass  6559  omordi  6564  nnmordi  6629  fiint  7133  zorn2lem6  8128  zorn2lem7  8129  mulgt0sr  8727  sqlecan  11209  rexuzre  11836  caurcvg  12149  ndvdssub  12606  lsmcv  15894  nrmsep3  17083  2ndcdisj  17182  2ndcsep  17185  tsmsxp  17837  metcnp3  18086  xrlimcnp  20263  elspansn4  22152  hoadddir  22384  atcvatlem  22965  sumdmdii  22995  sumdmdlem  22998  wfrlem12  24267  frrlem11  24293  ax5seglem5  24561  and4as  24939  iscnp4  25563  prtlem17  26744  onfrALTlem2  28311  in3an  28383  cvratlem  29610  athgt  29645  lplnnle2at  29730  lplncvrlvol2  29804  cdlemb  29983  dalaw  30075  cdleme50trn2  30740  cdlemg18b  30868  dihmeetlem3N  31495
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