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  6353  riotasv3dOLD  6354  oaass  6559  zorn2lem4  8126  zorn2lem7  8129  iscatd2  13583  fgss2  17569  alexsubALTlem4  17744  grporcan  20888  spansncvi  22231  mdsymlem5  22987  hbtlem2  26740  cvratlem  28983
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