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

Theorem exp42 594
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 587 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  ->  ( th 
->  ta ) ) )
32exp3a 425 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  isofrlem  5837  f1ocnv2d  6068  oelim  6533  zorn2lem7  8129  addid1  8992  issubg4  14638  lmodvsdir  15652  lmodvsass  15654  dvfsumrlim3  19380  shscli  21896  f1o3d  23037  cmpmor  25975  lshpcmp  29178
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator