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

This theorem is referenced by:  ad5ant2345  1367  tz7.49  8440  supxrun  13292  injresinj  13750  fi1uzind  14455  brfi1indALT  14458  swrdswrdlem  14651  swrdswrd  14652  2cshwcshw  14773  cshwcsh2id  14776  prmgaplem6  16988  cusgrsize2inds  29179  usgr2pthlem  29489  usgr2pth  29490  elwwlks2  29689  rusgrnumwwlks  29697  clwlkclwwlklem2a4  29719  clwlkclwwlklem2  29722  umgrhashecclwwlk  29800  1to3vfriswmgr  30002  frgrnbnb  30015  branmfn  31827  elrspunidl  33015  zarcmplem  33350  relowlpssretop  36735  broucube  37012  eel0000  43970  eel00001  43971  eel00000  43972  eel11111  43973  climrec  44804  bgoldbtbndlem4  46961  bgoldbtbnd  46962  tgoldbach  46970  isomuspgr  46987  2zlidl  47103  2zrngmmgm  47115  lincsumcl  47300