Theorem exp41 433

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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  ad5ant2345  1368  tz7.49  8449  supxrun  13301  injresinj  13759  fi1uzind  14464  brfi1indALT  14467  swrdswrdlem  14660  swrdswrd  14661  2cshwcshw  14782  cshwcsh2id  14785  prmgaplem6  16995  cusgrsize2inds  28975  usgr2pthlem  29285  usgr2pth  29286  elwwlks2  29485  rusgrnumwwlks  29493  clwlkclwwlklem2a4  29515  clwlkclwwlklem2  29518  umgrhashecclwwlk  29596  1to3vfriswmgr  29798  frgrnbnb  29811  branmfn  31623  elrspunidl  32818  zarcmplem  33157  relowlpssretop  36550  broucube  36827  eel0000  43785  eel00001  43786  eel00000  43787  eel11111  43788  climrec  44619  bgoldbtbndlem4  46776  bgoldbtbnd  46777  tgoldbach  46785  isomuspgr  46802  2zlidl  46922  2zrngmmgm  46934  lincsumcl  47201