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  4567  riotasv2dOLD  6554  tfr3  6619  oaass  6763  omordi  6768  nnmordi  6833  fiint  7342  zorn2lem6  8337  zorn2lem7  8338  mulgt0sr  8936  sqlecan  11442  rexuzre  12111  caurcvg  12425  ndvdssub  12882  lsmcv  16168  iscnp4  17281  nrmsep3  17373  2ndcdisj  17472  2ndcsep  17475  tsmsxp  18137  metcnp3  18523  xrlimcnp  20760  elspansn4  23028  hoadddir  23260  atcvatlem  23841  sumdmdii  23871  sumdmdlem  23874  wfrlem12  25481  frrlem11  25507  ax5seglem5  25776  prtlem17  26615  onfrALTlem2  28343  in3an  28421  cvratlem  29903  athgt  29938  lplnnle2at  30023  lplncvrlvol2  30097  cdlemb  30276  dalaw  30368  cdleme50trn2  31033  cdlemg18b  31161  dihmeetlem3N  31788
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