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  1398  tz7.49  8493  supxrun  13486  injresinj  13966  fi1uzind  14693  brfi1indALT  14696  swrdswrdlem  14895  swrdswrd  14896  2cshwcshw  15018  cshwcsh2id  15021  prmgaplem6  17278  cusgrsize2inds  30091  usgr2pthlem  30406  usgr2pth  30407  elwwlks2  30615  rusgrnumwwlks  30623  clwlkclwwlklem2a4  30645  clwlkclwwlklem2  30648  umgrhashecclwwlk  30726  1to3vfriswmgr  30938  frgrnbnb  30951  branmfn  32764  dfufd2lem  34185  zarcmplem  34624  relowlpssretop  38555  broucube  38840  eel0000  45962  eel00001  45963  eel00000  45964  eel11111  45965  climrec  46888  bgoldbtbndlem4  49179  bgoldbtbnd  49180  tgoldbach  49188  2zlidl  49610  2zrngmmgm  49622  lincsumcl  49874