Theorem exp41 437

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  ad5ant2345  1366  tz7.49  8075  supxrun  12703  injresinj  13152  fi1uzind  13849  brfi1indALT  13852  swrdswrdlem  14060  swrdswrd  14061  2cshwcshw  14181  cshwcsh2id  14184  prmgaplem6  16386  cusgrsize2inds  27229  usgr2pthlem  27538  usgr2pth  27539  elwwlks2  27739  rusgrnumwwlks  27747  clwlkclwwlklem2a4  27769  clwlkclwwlklem2  27772  umgrhashecclwwlk  27851  1to3vfriswmgr  28053  frgrnbnb  28066  branmfn  29876  relowlpssretop  34639  broucube  34920  eel0000  41047  eel00001  41048  eel00000  41049  eel11111  41050  climrec  41877  bgoldbtbndlem4  43967  bgoldbtbnd  43968  tgoldbach  43976  isomuspgr  43993  2zlidl  44199  2zrngmmgm  44211  lincsumcl  44480