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

Theorem exp4c 608
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 ) )
21expd 436 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  ->  ( th 
->  ta ) ) )
32expd 436 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  oawordri  7094  oaordex  7102  odi  7123  pssnn  7637  alephval3  8386  dfac2  8406  axdc4lem  8730  leexp1a  12034  wrdsymb0  12372  swrdvalodm2  12446  swrdvalodm  12447  2ndcctbss  19186  atcvatlem  25936  exp5g  28639  exp5j  28640  wwlknext  30499  frgraregord013  30854  lmodvsmdi  30962  lmodvsmmulgdi  30963  assamulgscm  30972  lindslinindsimp1  31105  cdleme48gfv1  34499  cdlemg6e  34585  dihord5apre  35226  dihglblem5apreN  35255
  Copyright terms: Public domain W3C validator