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

Theorem exp42 611
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
exp42.1  |-  ( ( ( ph  /\  ( ps  /\  ch ) )  /\  th )  ->  ta )
Assertion
Ref Expression
exp42  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )

Proof of Theorem exp42
StepHypRef Expression
1 exp42.1 . . 3  |-  ( ( ( ph  /\  ( ps  /\  ch ) )  /\  th )  ->  ta )
21exp31 604 . 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:  isofrlem  6217  f1ocnv2d  6507  oelim  7182  zorn2lem7  8880  addid1  9758  issubg4  16089  lmodvsdir  17404  lmodvsass  17405  gsummatr01lem4  19027  dvfsumrlim3  22300  shscli  26100  f1o3d  27336  slmdvsdir  27625  slmdvsass  27626  lshpcmp  34415
  Copyright terms: Public domain W3C validator