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  4403  tz7.7  4434  oalimcl  6574  unbenlem  12971  rnelfm  17664  spansncvi  22247  atom1d  22949  chirredlem3  22988  finminlem  26334  cvlcvr1  30151  lhpexle2lem  30820  trlord  31380  cdlemkid4  31745  dihord6apre  32068  dihglbcpreN  32112
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