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  4434  riotasv2dOLD  6366  tfr3  6431  oaass  6575  omordi  6580  nnmordi  6645  fiint  7149  zorn2lem6  8144  zorn2lem7  8145  mulgt0sr  8743  sqlecan  11225  rexuzre  11852  caurcvg  12165  ndvdssub  12622  lsmcv  15910  nrmsep3  17099  2ndcdisj  17198  2ndcsep  17201  tsmsxp  17853  metcnp3  18102  xrlimcnp  20279  elspansn4  22168  hoadddir  22400  atcvatlem  22981  sumdmdii  23011  sumdmdlem  23014  wfrlem12  24338  frrlem11  24364  ax5seglem5  24633  and4as  25042  iscnp4  25666  prtlem17  26847  onfrALTlem2  28610  in3an  28688  cvratlem  30232  athgt  30267  lplnnle2at  30352  lplncvrlvol2  30426  cdlemb  30605  dalaw  30697  cdleme50trn2  31362  cdlemg18b  31490  dihmeetlem3N  32117
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