Theorem exp41 434

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  ad5ant2345  1372  tz7.49  8374  supxrun  13237  injresinj  13710  fi1uzind  14433  brfi1indALT  14436  swrdswrdlem  14629  swrdswrd  14630  2cshwcshw  14751  cshwcsh2id  14754  prmgaplem6  16987  cusgrsize2inds  29418  usgr2pthlem  29727  usgr2pth  29728  elwwlks2  29930  rusgrnumwwlks  29938  clwlkclwwlklem2a4  29960  clwlkclwwlklem2  29963  umgrhashecclwwlk  30041  1to3vfriswmgr  30243  frgrnbnb  30256  branmfn  32068  elrspunidl  33384  dfufd2lem  33505  zarcmplem  33867  relowlpssretop  37357  broucube  37653  eel0000  44713  eel00001  44714  eel00000  44715  eel11111  44716  climrec  45604  bgoldbtbndlem4  47812  bgoldbtbnd  47813  tgoldbach  47821  2zlidl  48244  2zrngmmgm  48256  lincsumcl  48436