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

Theorem exp4a 603
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 444 . 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  604  exp4d  606  exp45  611  exp5c  613  tz7.7  4741  tfr3  6854  oaass  6996  omordi  7001  nnmordi  7066  fiint  7584  zorn2lem6  8666  zorn2lem7  8667  mulgt0sr  9268  sqlecan  11968  rexuzre  12836  caurcvg  13150  ndvdssub  13607  lsmcv  17200  iscnp4  18826  nrmsep3  18918  2ndcdisj  19019  2ndcsep  19022  tsmsxp  19688  metcnp3  20074  xrlimcnp  22321  ax5seglem5  23114  elspansn4  24911  hoadddir  25143  atcvatlem  25724  sumdmdii  25754  sumdmdlem  25757  wfrlem12  27664  frrlem11  27709  prtlem17  28946  lindslinindsimp1  30832  onfrALTlem2  31087  in3an  31167  cvratlem  32787  athgt  32822  lplnnle2at  32907  lplncvrlvol2  32981  cdlemb  33160  dalaw  33252  cdleme50trn2  33917  cdlemg18b  34045  dihmeetlem3N  34672
  Copyright terms: Public domain W3C validator