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  4745  tfr3  6858  oaass  7000  omordi  7005  nnmordi  7070  fiint  7588  zorn2lem6  8670  zorn2lem7  8671  mulgt0sr  9272  sqlecan  11972  rexuzre  12840  caurcvg  13154  ndvdssub  13611  lsmcv  17222  iscnp4  18867  nrmsep3  18959  2ndcdisj  19060  2ndcsep  19063  tsmsxp  19729  metcnp3  20115  xrlimcnp  22362  ax5seglem5  23179  elspansn4  24976  hoadddir  25208  atcvatlem  25789  sumdmdii  25819  sumdmdlem  25822  wfrlem12  27735  frrlem11  27780  prtlem17  29021  lindslinindsimp1  30991  onfrALTlem2  31254  in3an  31333  cvratlem  33065  athgt  33100  lplnnle2at  33185  lplncvrlvol2  33259  cdlemb  33438  dalaw  33530  cdleme50trn2  34195  cdlemg18b  34323  dihmeetlem3N  34950
  Copyright terms: Public domain W3C validator