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

Theorem exp4a 604
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 367
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 369
This theorem is referenced by:  exp4b  605  exp4d  607  exp45  612  exp5c  614  tz7.7  5436  wfrlem12  7032  tfr3  7102  oaass  7247  omordi  7252  nnmordi  7317  fiint  7831  zorn2lem6  8913  zorn2lem7  8914  mulgt0sr  9512  sqlecan  12319  rexuzre  13334  caurcvg  13648  ndvdssub  14274  lsmcv  18107  iscnp4  20057  nrmsep3  20149  2ndcdisj  20249  2ndcsep  20252  tsmsxp  20949  metcnp3  21335  xrlimcnp  23624  ax5seglem5  24653  elspansn4  26905  hoadddir  27136  atcvatlem  27717  sumdmdii  27747  sumdmdlem  27750  frrlem11  30099  isbasisrelowllem1  31272  isbasisrelowllem2  31273  prtlem17  31899  cvratlem  32438  athgt  32473  lplnnle2at  32558  lplncvrlvol2  32632  cdlemb  32811  dalaw  32903  cdleme50trn2  33570  cdlemg18b  33698  dihmeetlem3N  34325  onfrALTlem2  36342  in3an  36421  lindslinindsimp1  38569
  Copyright terms: Public domain W3C validator