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  8390  supxrun  13252  injresinj  13725  fi1uzind  14448  brfi1indALT  14451  swrdswrdlem  14645  swrdswrd  14646  2cshwcshw  14767  cshwcsh2id  14770  prmgaplem6  17003  cusgrsize2inds  29357  usgr2pthlem  29666  usgr2pth  29667  elwwlks2  29869  rusgrnumwwlks  29877  clwlkclwwlklem2a4  29899  clwlkclwwlklem2  29902  umgrhashecclwwlk  29980  1to3vfriswmgr  30182  frgrnbnb  30195  branmfn  32007  elrspunidl  33372  dfufd2lem  33493  zarcmplem  33844  relowlpssretop  37325  broucube  37621  eel0000  44682  eel00001  44683  eel00000  44684  eel11111  44685  climrec  45574  bgoldbtbndlem4  47782  bgoldbtbnd  47783  tgoldbach  47791  2zlidl  48201  2zrngmmgm  48213  lincsumcl  48393