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

Theorem exp41 595
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 425 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  -> 
( th  ->  ta ) )
32exp31 589 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  tz7.49  6704  supxrun  10896  injresinj  11202  brfi1uzind  11717  cusgrasize2inds  21488  3v3e3cycl1  21633  constr3cycl  21650  4cycl4v4e  21655  4cycl4dv4e  21657  branmfn  23610  climrec  27707  swrdswrdlem  28220  swrdswrd  28221  usgra2pthspth  28331  usgra2wlkspthlem2  28333  usgra2pthlem1  28336  el2wlkonot  28389  2spontn0vne  28407  1to3vfriswmgra  28459  frgranbnb  28472  frgrawopreg  28500  usg2spot2nb  28516  ad5ant1345  28624  ad5ant2345  28625  eel0001  28892  eel0000  28893  eel1111  28894  eel00001  28895  eel00000  28896  eel11111  28897
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 179  df-an 362
  Copyright terms: Public domain W3C validator