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

Theorem exp4a 606
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 446 . 2  |-  ( ( ( ch  /\  th )  ->  ta )  <->  ( ch  ->  ( th  ->  ta ) ) )
31, 2syl6ib 226 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  exp4b  607  exp4d  609  exp45  614  exp5c  616  tz7.7  4894  tfr3  7070  oaass  7212  omordi  7217  nnmordi  7282  fiint  7799  zorn2lem6  8884  zorn2lem7  8885  mulgt0sr  9485  sqlecan  12253  rexuzre  13164  caurcvg  13478  ndvdssub  13942  lsmcv  17661  iscnp4  19637  nrmsep3  19729  2ndcdisj  19830  2ndcsep  19833  tsmsxp  20530  metcnp3  20916  xrlimcnp  23170  ax5seglem5  24108  elspansn4  26363  hoadddir  26595  atcvatlem  27176  sumdmdii  27206  sumdmdlem  27209  wfrlem12  29329  frrlem11  29374  prtlem17  30592  lindslinindsimp1  32788  onfrALTlem2  33046  in3an  33125  cvratlem  34879  athgt  34914  lplnnle2at  34999  lplncvrlvol2  35073  cdlemb  35252  dalaw  35344  cdleme50trn2  36011  cdlemg18b  36139  dihmeetlem3N  36766
  Copyright terms: Public domain W3C validator