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

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

Proof of Theorem exp44
StepHypRef Expression
1 exp44.1 . . 3  |-  ( (
ph  /\  ( ( ps  /\  ch )  /\  th ) )  ->  ta )
21exp32 588 . 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:  wefrc  4387  tz7.7  4418  oalimcl  6558  unbenlem  12955  rnelfm  17648  spansncvi  22231  atom1d  22933  chirredlem3  22972  finminlem  26231  cvlcvr1  29529  lhpexle2lem  30198  trlord  30758  cdlemkid4  31123  dihord6apre  31446  dihglbcpreN  31490
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