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

Theorem exp4c 592
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 426 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  ->  ( th 
->  ta ) ) )
32exp3a 426 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  tfrlem1  6595  oawordri  6752  oaordex  6760  odi  6781  pssnn  7286  alephval3  7947  dfac2  7967  axdc4lem  8291  leexp1a  11393  2ndcctbss  17471  atcvatlem  23841  exp5g  26194  exp5j  26195  cdleme48gfv1  31018  cdlemg6e  31104  dihord5apre  31745  dihglblem5apreN  31774
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