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  1372  tz7.49  8359  supxrun  13210  injresinj  13686  fi1uzind  14409  brfi1indALT  14412  swrdswrdlem  14606  swrdswrd  14607  2cshwcshw  14727  cshwcsh2id  14730  prmgaplem6  16963  cusgrsize2inds  29427  usgr2pthlem  29736  usgr2pth  29737  elwwlks2  29939  rusgrnumwwlks  29947  clwlkclwwlklem2a4  29969  clwlkclwwlklem2  29972  umgrhashecclwwlk  30050  1to3vfriswmgr  30252  frgrnbnb  30265  branmfn  32077  elrspunidl  33385  dfufd2lem  33506  zarcmplem  33886  relowlpssretop  37398  broucube  37694  eel0000  44752  eel00001  44753  eel00000  44754  eel11111  44755  climrec  45643  bgoldbtbndlem4  47839  bgoldbtbnd  47840  tgoldbach  47848  2zlidl  48271  2zrngmmgm  48283  lincsumcl  48463