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  8416  supxrun  13283  injresinj  13756  fi1uzind  14479  brfi1indALT  14482  swrdswrdlem  14676  swrdswrd  14677  2cshwcshw  14798  cshwcsh2id  14801  prmgaplem6  17034  cusgrsize2inds  29388  usgr2pthlem  29700  usgr2pth  29701  elwwlks2  29903  rusgrnumwwlks  29911  clwlkclwwlklem2a4  29933  clwlkclwwlklem2  29936  umgrhashecclwwlk  30014  1to3vfriswmgr  30216  frgrnbnb  30229  branmfn  32041  elrspunidl  33406  dfufd2lem  33527  zarcmplem  33878  relowlpssretop  37359  broucube  37655  eel0000  44716  eel00001  44717  eel00000  44718  eel11111  44719  climrec  45608  bgoldbtbndlem4  47813  bgoldbtbnd  47814  tgoldbach  47822  2zlidl  48232  2zrngmmgm  48244  lincsumcl  48424