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

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

Proof of Theorem exp4c
StepHypRef Expression
1 exp4c.1 . . 3  |-  ( ph  ->  ( ( ( ps 
/\  ch )  /\  th )  ->  ta ) )
21exp3a 425 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  ->  ( th 
->  ta ) ) )
32exp3a 425 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  tfrlem1  6391  oawordri  6548  oaordex  6556  odi  6577  pssnn  7081  alephval3  7737  dfac2  7757  axdc4lem  8081  leexp1a  11160  2ndcctbss  17181  atcvatlem  22965  exp5g  26209  exp5j  26210  cdleme48gfv1  30725  cdlemg6e  30811  dihord5apre  31452  dihglblem5apreN  31481
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