MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exp4a Structured version   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  4599  riotasv2dOLD  6587  tfr3  6652  oaass  6796  omordi  6801  nnmordi  6866  fiint  7375  zorn2lem6  8373  zorn2lem7  8374  mulgt0sr  8972  sqlecan  11479  rexuzre  12148  caurcvg  12462  ndvdssub  12919  lsmcv  16205  iscnp4  17319  nrmsep3  17411  2ndcdisj  17511  2ndcsep  17514  tsmsxp  18176  metcnp3  18562  xrlimcnp  20799  elspansn4  23067  hoadddir  23299  atcvatlem  23880  sumdmdii  23910  sumdmdlem  23913  wfrlem12  25541  frrlem11  25586  ax5seglem5  25864  prtlem17  26716  onfrALTlem2  28569  in3an  28649  cvratlem  30155  athgt  30190  lplnnle2at  30275  lplncvrlvol2  30349  cdlemb  30528  dalaw  30620  cdleme50trn2  31285  cdlemg18b  31413  dihmeetlem3N  32040
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