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  8448  supxrun  13439  injresinj  13919  fi1uzind  14645  brfi1indALT  14648  swrdswrdlem  14846  swrdswrd  14847  2cshwcshw  14969  cshwcsh2id  14972  prmgaplem6  17227  cusgrsize2inds  30027  usgr2pthlem  30342  usgr2pth  30343  elwwlks2  30551  rusgrnumwwlks  30559  clwlkclwwlklem2a4  30581  clwlkclwwlklem2  30584  umgrhashecclwwlk  30662  1to3vfriswmgr  30874  frgrnbnb  30887  branmfn  32700  elrspunidl  33971  dfufd2lem  34074  zarcmplem  34506  relowlpssretop  38267  broucube  38552  eel0000  45687  eel00001  45688  eel00000  45689  eel11111  45690  climrec  46584  bgoldbtbndlem4  48875  bgoldbtbnd  48876  tgoldbach  48884  2zlidl  49306  2zrngmmgm  49318  lincsumcl  49512