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  8459  supxrun  13332  injresinj  13804  fi1uzind  14525  brfi1indALT  14528  swrdswrdlem  14722  swrdswrd  14723  2cshwcshw  14844  cshwcsh2id  14847  prmgaplem6  17076  cusgrsize2inds  29433  usgr2pthlem  29745  usgr2pth  29746  elwwlks2  29948  rusgrnumwwlks  29956  clwlkclwwlklem2a4  29978  clwlkclwwlklem2  29981  umgrhashecclwwlk  30059  1to3vfriswmgr  30261  frgrnbnb  30274  branmfn  32086  elrspunidl  33443  dfufd2lem  33564  zarcmplem  33912  relowlpssretop  37382  broucube  37678  eel0000  44744  eel00001  44745  eel00000  44746  eel11111  44747  climrec  45632  bgoldbtbndlem4  47822  bgoldbtbnd  47823  tgoldbach  47831  2zlidl  48215  2zrngmmgm  48227  lincsumcl  48407