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  6235  f1ocnv2d  6521  oelim  7196  zorn2lem7  8894  addid1  9771  issubg4  16092  lmodvsdir  17407  lmodvsass  17408  gsummatr01lem4  19029  dvfsumrlim3  22302  shscli  26058  f1o3d  27294  slmdvsdir  27583  slmdvsass  27584  lshpcmp  34186
  Copyright terms: Public domain W3C validator