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

This theorem is referenced by:  ad5ant2345  1368  tz7.49  8246  supxrun  12979  injresinj  13436  fi1uzind  14139  brfi1indALT  14142  swrdswrdlem  14345  swrdswrd  14346  2cshwcshw  14466  cshwcsh2id  14469  prmgaplem6  16685  cusgrsize2inds  27723  usgr2pthlem  28032  usgr2pth  28033  elwwlks2  28232  rusgrnumwwlks  28240  clwlkclwwlklem2a4  28262  clwlkclwwlklem2  28265  umgrhashecclwwlk  28343  1to3vfriswmgr  28545  frgrnbnb  28558  branmfn  30368  elrspunidl  31508  zarcmplem  31733  relowlpssretop  35462  broucube  35738  eel0000  42229  eel00001  42230  eel00000  42231  eel11111  42232  climrec  43034  bgoldbtbndlem4  45148  bgoldbtbnd  45149  tgoldbach  45157  isomuspgr  45174  2zlidl  45380  2zrngmmgm  45392  lincsumcl  45660