Theorem exp41 440

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 418	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → (𝜃 → 𝜏))
3	2	exp31 425	1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ad5ant2345  1397  tz7.49  8438  supxrun  13358  injresinj  13837  fi1uzind  14562  brfi1indALT  14565  swrdswrdlem  14763  swrdswrd  14764  2cshwcshw  14886  cshwcsh2id  14889  prmgaplem6  17138  cusgrsize2inds  29861  usgr2pthlem  30176  usgr2pth  30177  elwwlks2  30385  rusgrnumwwlks  30393  clwlkclwwlklem2a4  30415  clwlkclwwlklem2  30418  umgrhashecclwwlk  30496  1to3vfriswmgr  30702  frgrnbnb  30715  branmfn  32528  elrspunidl  33800  dfufd2lem  33903  zarcmplem  34335  relowlpssretop  38067  broucube  38362  eel0000  45486  eel00001  45487  eel00000  45488  eel11111  45489  climrec  46377  bgoldbtbndlem4  48631  bgoldbtbnd  48632  tgoldbach  48640  2zlidl  49062  2zrngmmgm  49074  lincsumcl  49268