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  1369  tz7.49  8484  supxrun  13355  injresinj  13824  fi1uzind  14543  brfi1indALT  14546  swrdswrdlem  14739  swrdswrd  14740  2cshwcshw  14861  cshwcsh2id  14864  prmgaplem6  17090  cusgrsize2inds  29486  usgr2pthlem  29796  usgr2pth  29797  elwwlks2  29996  rusgrnumwwlks  30004  clwlkclwwlklem2a4  30026  clwlkclwwlklem2  30029  umgrhashecclwwlk  30107  1to3vfriswmgr  30309  frgrnbnb  30322  branmfn  32134  elrspunidl  33436  dfufd2lem  33557  zarcmplem  33842  relowlpssretop  37347  broucube  37641  eel0000  44718  eel00001  44719  eel00000  44720  eel11111  44721  climrec  45559  bgoldbtbndlem4  47733  bgoldbtbnd  47734  tgoldbach  47742  2zlidl  48084  2zrngmmgm  48096  lincsumcl  48277