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 208  df-an 397

This theorem is referenced by:  ad5ant2345  1378  tz7.49  8374  supxrun  13259  injresinj  13737  fi1uzind  14460  brfi1indALT  14463  swrdswrdlem  14657  swrdswrd  14658  2cshwcshw  14778  cshwcsh2id  14781  prmgaplem6  17018  cusgrsize2inds  29540  usgr2pthlem  29849  usgr2pth  29850  elwwlks2  30055  rusgrnumwwlks  30063  clwlkclwwlklem2a4  30085  clwlkclwwlklem2  30088  umgrhashecclwwlk  30166  1to3vfriswmgr  30368  frgrnbnb  30381  branmfn  32194  elrspunidl  33511  dfufd2lem  33632  zarcmplem  34065  relowlpssretop  37726  broucube  38021  eel0000  45163  eel00001  45164  eel00000  45165  eel11111  45166  climrec  46048  bgoldbtbndlem4  48299  bgoldbtbnd  48300  tgoldbach  48308  2zlidl  48731  2zrngmmgm  48743  lincsumcl  48922