Theorem exp41 439

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  ad5ant2345  1395  tz7.49  8428  supxrun  13338  injresinj  13816  fi1uzind  14540  brfi1indALT  14543  swrdswrdlem  14737  swrdswrd  14738  2cshwcshw  14858  cshwcsh2id  14861  prmgaplem6  17112  cusgrsize2inds  29740  usgr2pthlem  30049  usgr2pth  30050  elwwlks2  30255  rusgrnumwwlks  30263  clwlkclwwlklem2a4  30285  clwlkclwwlklem2  30288  umgrhashecclwwlk  30366  1to3vfriswmgr  30568  frgrnbnb  30581  branmfn  32394  elrspunidl  33676  dfufd2lem  33780  zarcmplem  34212  relowlpssretop  37893  broucube  38188  eel0000  45315  eel00001  45316  eel00000  45317  eel11111  45318  climrec  46206  bgoldbtbndlem4  48457  bgoldbtbnd  48458  tgoldbach  48466  2zlidl  48889  2zrngmmgm  48901  lincsumcl  49091