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  1397  tz7.49  8428  supxrun  13337  injresinj  13816  fi1uzind  14540  brfi1indALT  14543  swrdswrdlem  14737  swrdswrd  14738  2cshwcshw  14858  cshwcsh2id  14861  prmgaplem6  17111  cusgrsize2inds  29803  usgr2pthlem  30112  usgr2pth  30113  elwwlks2  30318  rusgrnumwwlks  30326  clwlkclwwlklem2a4  30348  clwlkclwwlklem2  30351  umgrhashecclwwlk  30429  1to3vfriswmgr  30631  frgrnbnb  30644  branmfn  32457  elrspunidl  33736  dfufd2lem  33839  zarcmplem  34271  relowlpssretop  38010  broucube  38305  eel0000  45428  eel00001  45429  eel00000  45430  eel11111  45431  climrec  46319  bgoldbtbndlem4  48573  bgoldbtbnd  48574  tgoldbach  48582  2zlidl  49005  2zrngmmgm  49017  lincsumcl  49211