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

Step	Hyp	Ref	Expression
1		exp41.1	. . 3 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
2	1	ex 449	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → (𝜃 → 𝜏))
3	2	exp31 631	1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

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