Theorem exp41 440

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ad5ant2345  1397  tz7.49  8434  supxrun  13368  injresinj  13847  fi1uzind  14572  brfi1indALT  14575  swrdswrdlem  14773  swrdswrd  14774  2cshwcshw  14896  cshwcsh2id  14899  prmgaplem6  17148  cusgrsize2inds  29913  usgr2pthlem  30228  usgr2pth  30229  elwwlks2  30437  rusgrnumwwlks  30445  clwlkclwwlklem2a4  30467  clwlkclwwlklem2  30470  umgrhashecclwwlk  30548  1to3vfriswmgr  30760  frgrnbnb  30773  branmfn  32586  elrspunidl  33856  dfufd2lem  33959  zarcmplem  34391  relowlpssretop  38118  broucube  38403  eel0000  45542  eel00001  45543  eel00000  45544  eel11111  45545  climrec  46433  bgoldbtbndlem4  48724  bgoldbtbnd  48725  tgoldbach  48733  2zlidl  49155  2zrngmmgm  49167  lincsumcl  49361