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  1369  tz7.49  8276  supxrun  13050  injresinj  13508  fi1uzind  14211  brfi1indALT  14214  swrdswrdlem  14417  swrdswrd  14418  2cshwcshw  14538  cshwcsh2id  14541  prmgaplem6  16757  cusgrsize2inds  27820  usgr2pthlem  28131  usgr2pth  28132  elwwlks2  28331  rusgrnumwwlks  28339  clwlkclwwlklem2a4  28361  clwlkclwwlklem2  28364  umgrhashecclwwlk  28442  1to3vfriswmgr  28644  frgrnbnb  28657  branmfn  30467  elrspunidl  31606  zarcmplem  31831  relowlpssretop  35535  broucube  35811  eel0000  42340  eel00001  42341  eel00000  42342  eel11111  42343  climrec  43144  bgoldbtbndlem4  45260  bgoldbtbnd  45261  tgoldbach  45269  isomuspgr  45286  2zlidl  45492  2zrngmmgm  45504  lincsumcl  45772