Theorem exp41 438

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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  ad5ant2345  1388  tz7.49  8410  supxrun  13313  injresinj  13791  fi1uzind  14514  brfi1indALT  14517  swrdswrdlem  14711  swrdswrd  14712  2cshwcshw  14832  cshwcsh2id  14835  prmgaplem6  17083  cusgrsize2inds  29611  usgr2pthlem  29920  usgr2pth  29921  elwwlks2  30126  rusgrnumwwlks  30134  clwlkclwwlklem2a4  30156  clwlkclwwlklem2  30159  umgrhashecclwwlk  30237  1to3vfriswmgr  30439  frgrnbnb  30452  branmfn  32265  elrspunidl  33575  dfufd2lem  33706  zarcmplem  34139  relowlpssretop  37819  broucube  38114  eel0000  45256  eel00001  45257  eel00000  45258  eel11111  45259  climrec  46140  bgoldbtbndlem4  48391  bgoldbtbnd  48392  tgoldbach  48400  2zlidl  48823  2zrngmmgm  48835  lincsumcl  49014