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

Theorem exp44 597
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 589 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  ->  ( th 
->  ta ) ) )
32exp3a 426 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  wefrc  4519  tz7.7  4550  oalimcl  6741  unbenlem  13205  rnelfm  17908  spansncvi  23004  atom1d  23706  chirredlem3  23745  finminlem  26014  cvlcvr1  29456  lhpexle2lem  30125  trlord  30685  cdlemkid4  31050  dihord6apre  31373  dihglbcpreN  31417
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 178  df-an 361
  Copyright terms: Public domain W3C validator