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

Theorem exp44 611
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 603 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  ->  ( th 
->  ta ) ) )
32expd 434 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  wefrc  4862  tz7.7  4893  oalimcl  7201  unbenlem  14510  rnelfm  20620  wwlknimp  24889  spansncvi  26768  atom1d  27470  chirredlem3  27509  finminlem  30376  cvlcvr1  35461  lhpexle2lem  36130  trlord  36692  cdlemkid4  37057  dihord6apre  37380  dihglbcpreN  37424
  Copyright terms: Public domain W3C validator