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

Theorem exp4a 590
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 434 . 2  |-  ( ( ( ch  /\  th )  ->  ta )  <->  ( ch  ->  ( th  ->  ta ) ) )
31, 2syl6ib 218 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  exp4b  591  exp4d  593  exp45  598  exp5c  600  tz7.7  4541  riotasv2dOLD  6524  tfr3  6589  oaass  6733  omordi  6738  nnmordi  6803  fiint  7312  zorn2lem6  8307  zorn2lem7  8308  mulgt0sr  8906  sqlecan  11407  rexuzre  12076  caurcvg  12390  ndvdssub  12847  lsmcv  16133  iscnp4  17242  nrmsep3  17334  2ndcdisj  17433  2ndcsep  17436  tsmsxp  18098  metcnp3  18453  xrlimcnp  20667  elspansn4  22916  hoadddir  23148  atcvatlem  23729  sumdmdii  23759  sumdmdlem  23762  wfrlem12  25284  frrlem11  25310  ax5seglem5  25579  prtlem17  26409  onfrALTlem2  27968  in3an  28046  cvratlem  29586  athgt  29621  lplnnle2at  29706  lplncvrlvol2  29780  cdlemb  29959  dalaw  30051  cdleme50trn2  30716  cdlemg18b  30844  dihmeetlem3N  31471
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 178  df-an 361
  Copyright terms: Public domain W3C validator