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

Theorem exp4c 603
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 436 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  ->  ( th 
->  ta ) ) )
32exp3a 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  6977  oaordex  6985  odi  7006  pssnn  7519  alephval3  8268  dfac2  8288  axdc4lem  8612  leexp1a  11905  wrdsymb0  12242  swrdvalodm2  12316  swrdvalodm  12317  2ndcctbss  18900  atcvatlem  25611  exp5g  28337  exp5j  28338  wwlknext  30199  frgraregord013  30554  lindslinindsimp1  30697  cdleme48gfv1  33750  cdlemg6e  33836  dihord5apre  34477  dihglblem5apreN  34506
  Copyright terms: Public domain W3C validator