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

Theorem exp45 597
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
exp45.1  |-  ( (
ph  /\  ( ps  /\  ( ch  /\  th ) ) )  ->  ta )
Assertion
Ref Expression
exp45  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )

Proof of Theorem exp45
StepHypRef Expression
1 exp45.1 . . 3  |-  ( (
ph  /\  ( ps  /\  ( ch  /\  th ) ) )  ->  ta )
21exp32 588 . 2  |-  ( ph  ->  ( ps  ->  (
( ch  /\  th )  ->  ta ) ) )
32exp4a 589 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  riotasv3d  6369  riotasv3dOLD  6370  oaass  6575  zorn2lem4  8142  zorn2lem7  8145  iscatd2  13599  fgss2  17585  alexsubALTlem4  17760  grporcan  20904  spansncvi  22247  mdsymlem5  23003  hbtlem2  27431  cvratlem  30232
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator