Theorem exp41 435

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  ad5ant2345  1370  tz7.49  8396  supxrun  13245  injresinj  13703  fi1uzind  14408  brfi1indALT  14411  swrdswrdlem  14604  swrdswrd  14605  2cshwcshw  14726  cshwcsh2id  14729  prmgaplem6  16939  cusgrsize2inds  28464  usgr2pthlem  28774  usgr2pth  28775  elwwlks2  28974  rusgrnumwwlks  28982  clwlkclwwlklem2a4  29004  clwlkclwwlklem2  29007  umgrhashecclwwlk  29085  1to3vfriswmgr  29287  frgrnbnb  29300  branmfn  31110  elrspunidl  32279  zarcmplem  32551  relowlpssretop  35908  broucube  36185  eel0000  43124  eel00001  43125  eel00000  43126  eel11111  43127  climrec  43964  bgoldbtbndlem4  46120  bgoldbtbnd  46121  tgoldbach  46129  isomuspgr  46146  2zlidl  46352  2zrngmmgm  46364  lincsumcl  46632