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

Theorem exp45 598
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 589 . 2  |-  ( ph  ->  ( ps  ->  (
( ch  /\  th )  ->  ta ) ) )
32exp4a 590 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  riotasv3d  6528  riotasv3dOLD  6529  oaass  6734  zorn2lem4  8306  zorn2lem7  8309  iscatd2  13827  fgss2  17821  alexsubALTlem4  17996  grporcan  21651  spansncvi  22996  mdsymlem5  23752  hbtlem2  26991  cvratlem  29587
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 178  df-an 361
  Copyright terms: Public domain W3C validator