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  5853  f1ocnv2d  6084  oelim  6549  zorn2lem7  8145  addid1  9008  issubg4  14654  lmodvsdir  15668  lmodvsass  15670  dvfsumrlim3  19396  shscli  21912  f1o3d  23053  cmpmor  26078  lshpcmp  29800
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