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  7197  oaordex  7205  odi  7226  pssnn  7736  alephval3  8489  dfac2  8509  axdc4lem  8833  leexp1a  12198  wrdsymb0  12549  swrdvalodm2  12638  swrdvalodm  12639  lmodvsmmulgdi  17415  assamulgscm  17867  2ndcctbss  19822  wwlknext  24589  frgraregord013  24983  atcvatlem  27169  exp5g  30087  exp5j  30088  lmodvsmdi  32685  lindslinindsimp1  32768  cdleme48gfv1  35964  cdlemg6e  36050  dihord5apre  36691  dihglblem5apreN  36720
  Copyright terms: Public domain W3C validator