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  8460  supxrun  13451  injresinj  13931  fi1uzind  14657  brfi1indALT  14660  swrdswrdlem  14859  swrdswrd  14860  2cshwcshw  14982  cshwcsh2id  14985  prmgaplem6  17241  cusgrsize2inds  30041  usgr2pthlem  30356  usgr2pth  30357  elwwlks2  30565  rusgrnumwwlks  30573  clwlkclwwlklem2a4  30595  clwlkclwwlklem2  30598  umgrhashecclwwlk  30676  1to3vfriswmgr  30888  frgrnbnb  30901  branmfn  32714  dfufd2lem  34129  zarcmplem  34561  relowlpssretop  38394  broucube  38679  eel0000  45809  eel00001  45810  eel00000  45811  eel11111  45812  climrec  46722  bgoldbtbndlem4  49013  bgoldbtbnd  49014  tgoldbach  49022  2zlidl  49444  2zrngmmgm  49456  lincsumcl  49650