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

Theorem exp41 639
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
exp41.1 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
Assertion
Ref Expression
exp41 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))

Proof of Theorem exp41
StepHypRef Expression
1 exp41.1 . . 3 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
21ex 449 . 2 (((𝜑𝜓) ∧ 𝜒) → (𝜃𝜏))
32exp31 631 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  ad5ant2345  1436  tz7.49  7660  supxrun  12260  injresinj  12704  fi1uzind  13392  brfi1indALT  13395  swrdswrdlem  13580  swrdswrd  13581  2cshwcshw  13692  cshwcsh2id  13695  prmgaplem6  15883  cusgrsize2inds  26480  usgr2pthlem  26790  usgr2pth  26791  wwlksnext  26932  elwwlks2  27009  rusgrnumwwlks  27017  clwlkclwwlklem2a4  27041  clwlkclwwlklem2  27044  umgrhashecclwwlk  27130  clwlksfclwwlkOLD  27137  1to3vfriswmgr  27355  frgrnbnb  27368  branmfn  29194  relowlpssretop  33444  broucube  33675  eel0001  39364  eel0000  39365  eel1111  39366  eel00001  39367  eel00000  39368  eel11111  39369  climrec  40255  bgoldbtbndlem4  42123  bgoldbtbnd  42124  tgoldbach  42132  tgoldbachOLD  42139  2zlidl  42361  2zrngmmgm  42373  lincsumcl  42647
  Copyright terms: Public domain W3C validator