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  4904  tfr3  7068  oaass  7210  omordi  7215  nnmordi  7280  fiint  7796  zorn2lem6  8880  zorn2lem7  8881  mulgt0sr  9481  sqlecan  12241  rexuzre  13147  caurcvg  13461  ndvdssub  13923  lsmcv  17582  iscnp4  19546  nrmsep3  19638  2ndcdisj  19739  2ndcsep  19742  tsmsxp  20408  metcnp3  20794  xrlimcnp  23042  ax5seglem5  23928  elspansn4  26183  hoadddir  26415  atcvatlem  26996  sumdmdii  27026  sumdmdlem  27029  wfrlem12  28947  frrlem11  28992  prtlem17  30237  lindslinindsimp1  32148  onfrALTlem2  32407  in3an  32486  cvratlem  34226  athgt  34261  lplnnle2at  34346  lplncvrlvol2  34420  cdlemb  34599  dalaw  34691  cdleme50trn2  35356  cdlemg18b  35484  dihmeetlem3N  36111
  Copyright terms: Public domain W3C validator