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  6475  oawordri  6632  oaordex  6640  odi  6661  pssnn  7166  alephval3  7824  dfac2  7844  axdc4lem  8168  leexp1a  11250  2ndcctbss  17281  atcvatlem  23073  exp5g  25533  exp5j  25534  cdleme48gfv1  30777  cdlemg6e  30863  dihord5apre  31504  dihglblem5apreN  31533
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