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  8376  supxrun  13231  injresinj  13707  fi1uzind  14430  brfi1indALT  14433  swrdswrdlem  14627  swrdswrd  14628  2cshwcshw  14748  cshwcsh2id  14751  prmgaplem6  16984  cusgrsize2inds  29527  usgr2pthlem  29836  usgr2pth  29837  elwwlks2  30042  rusgrnumwwlks  30050  clwlkclwwlklem2a4  30072  clwlkclwwlklem2  30075  umgrhashecclwwlk  30153  1to3vfriswmgr  30355  frgrnbnb  30368  branmfn  32180  elrspunidl  33509  dfufd2lem  33630  zarcmplem  34038  relowlpssretop  37569  broucube  37855  eel0000  44960  eel00001  44961  eel00000  44962  eel11111  44963  climrec  45849  bgoldbtbndlem4  48054  bgoldbtbnd  48055  tgoldbach  48063  2zlidl  48486  2zrngmmgm  48498  lincsumcl  48677