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

Theorem exp44 613
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 605 . 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:  wefrc  4825  tz7.7  4856  oalimcl  7112  unbenlem  14090  rnelfm  19661  spansncvi  25227  atom1d  25929  chirredlem3  25968  finminlem  28681  wwlknimp  30489  cvlcvr1  33342  lhpexle2lem  34011  trlord  34571  cdlemkid4  34936  dihord6apre  35259  dihglbcpreN  35303
  Copyright terms: Public domain W3C validator