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  6143  f1ocnv2d  6424  oelim  7087  zorn2lem7  8786  addid1  9664  issubg4  15823  lmodvsdir  17105  lmodvsass  17106  gsummatr01lem4  18606  dvfsumrlim3  21648  shscli  24899  f1o3d  26126  slmdvsdir  26404  slmdvsass  26405  lshpcmp  32996
  Copyright terms: Public domain W3C validator