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

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

Proof of Theorem exp41
StepHypRef Expression
1 exp41.1 . . 3  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ta )
21ex 423 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  -> 
( th  ->  ta ) )
32exp31 587 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  tz7.49  6473  supxrun  10650  branmfn  22701  injresinj  28215  3v3e3cycl1  28390  constr3cycl  28407  4cycl4v4e  28412  4cycl4dv4e  28414  1to3vfriswmgra  28431  ad5ant1345  28543  ad5ant2345  28544  eel0001  28807  eel0000  28808  eel1111  28809  eel00001  28810  eel00000  28811  eel11111  28812
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