MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exp45 Structured version   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  6590  riotasv3dOLD  6591  oaass  6796  zorn2lem4  8371  zorn2lem7  8374  iscatd2  13898  fgss2  17898  alexsubALTlem4  18073  grporcan  21801  spansncvi  23146  mdsymlem5  23902  hbtlem2  27296  cvratlem  30155
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