Theorem exp41 438

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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  ad5ant2345  1367  tz7.49  8064  supxrun  12697  injresinj  13153  fi1uzind  13851  brfi1indALT  13854  swrdswrdlem  14057  swrdswrd  14058  2cshwcshw  14178  cshwcsh2id  14181  prmgaplem6  16382  cusgrsize2inds  27243  usgr2pthlem  27552  usgr2pth  27553  elwwlks2  27752  rusgrnumwwlks  27760  clwlkclwwlklem2a4  27782  clwlkclwwlklem2  27785  umgrhashecclwwlk  27863  1to3vfriswmgr  28065  frgrnbnb  28078  branmfn  29888  elrspunidl  31014  zarcmplem  31234  relowlpssretop  34781  broucube  35091  eel0000  41426  eel00001  41427  eel00000  41428  eel11111  41429  climrec  42245  bgoldbtbndlem4  44326  bgoldbtbnd  44327  tgoldbach  44335  isomuspgr  44352  2zlidl  44558  2zrngmmgm  44570  lincsumcl  44840