Theorem exp41 434

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  ad5ant2345  1373  tz7.49  8384  supxrun  13268  injresinj  13746  fi1uzind  14469  brfi1indALT  14472  swrdswrdlem  14666  swrdswrd  14667  2cshwcshw  14787  cshwcsh2id  14790  prmgaplem6  17027  cusgrsize2inds  29522  usgr2pthlem  29831  usgr2pth  29832  elwwlks2  30037  rusgrnumwwlks  30045  clwlkclwwlklem2a4  30067  clwlkclwwlklem2  30070  umgrhashecclwwlk  30148  1to3vfriswmgr  30350  frgrnbnb  30363  branmfn  32176  elrspunidl  33488  dfufd2lem  33609  zarcmplem  34025  relowlpssretop  37680  broucube  37975  eel0000  45146  eel00001  45147  eel00000  45148  eel11111  45149  climrec  46033  bgoldbtbndlem4  48284  bgoldbtbnd  48285  tgoldbach  48293  2zlidl  48716  2zrngmmgm  48728  lincsumcl  48907