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  8413  supxrun  13276  injresinj  13749  fi1uzind  14472  brfi1indALT  14475  swrdswrdlem  14669  swrdswrd  14670  2cshwcshw  14791  cshwcsh2id  14794  prmgaplem6  17027  cusgrsize2inds  29381  usgr2pthlem  29693  usgr2pth  29694  elwwlks2  29896  rusgrnumwwlks  29904  clwlkclwwlklem2a4  29926  clwlkclwwlklem2  29929  umgrhashecclwwlk  30007  1to3vfriswmgr  30209  frgrnbnb  30222  branmfn  32034  elrspunidl  33399  dfufd2lem  33520  zarcmplem  33871  relowlpssretop  37352  broucube  37648  eel0000  44709  eel00001  44710  eel00000  44711  eel11111  44712  climrec  45601  bgoldbtbndlem4  47809  bgoldbtbnd  47810  tgoldbach  47818  2zlidl  48228  2zrngmmgm  48240  lincsumcl  48420