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

Theorem exp4c 606
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 434 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  ->  ( th 
->  ta ) ) )
32expd 434 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  oawordri  7191  oaordex  7199  odi  7220  pssnn  7731  alephval3  8482  dfac2  8502  axdc4lem  8826  leexp1a  12209  wrdsymb0  12566  swrdnd2  12652  lmodvsmmulgdi  17745  assamulgscm  18197  2ndcctbss  20125  wwlknext  24929  frgraregord013  25323  atcvatlem  27505  exp5g  30362  exp5j  30363  lmodvsmdi  33248  lindslinindsimp1  33331  nn0sumshdiglemB  33514  cdleme48gfv1  36678  cdlemg6e  36764  dihord5apre  37405  dihglblem5apreN  37434
  Copyright terms: Public domain W3C validator