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  1373  tz7.49  8377  supxrun  13259  injresinj  13737  fi1uzind  14460  brfi1indALT  14463  swrdswrdlem  14657  swrdswrd  14658  2cshwcshw  14778  cshwcsh2id  14781  prmgaplem6  17018  cusgrsize2inds  29537  usgr2pthlem  29846  usgr2pth  29847  elwwlks2  30052  rusgrnumwwlks  30060  clwlkclwwlklem2a4  30082  clwlkclwwlklem2  30085  umgrhashecclwwlk  30163  1to3vfriswmgr  30365  frgrnbnb  30378  branmfn  32191  elrspunidl  33503  dfufd2lem  33624  zarcmplem  34041  relowlpssretop  37694  broucube  37989  eel0000  45164  eel00001  45165  eel00000  45166  eel11111  45167  climrec  46051  bgoldbtbndlem4  48296  bgoldbtbnd  48297  tgoldbach  48305  2zlidl  48728  2zrngmmgm  48740  lincsumcl  48919