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  1370  tz7.49  8501  supxrun  13378  injresinj  13838  fi1uzind  14556  brfi1indALT  14559  swrdswrdlem  14752  swrdswrd  14753  2cshwcshw  14874  cshwcsh2id  14877  prmgaplem6  17103  cusgrsize2inds  29489  usgr2pthlem  29799  usgr2pth  29800  elwwlks2  29999  rusgrnumwwlks  30007  clwlkclwwlklem2a4  30029  clwlkclwwlklem2  30032  umgrhashecclwwlk  30110  1to3vfriswmgr  30312  frgrnbnb  30325  branmfn  32137  elrspunidl  33421  dfufd2lem  33542  zarcmplem  33827  relowlpssretop  37330  broucube  37614  eel0000  44691  eel00001  44692  eel00000  44693  eel11111  44694  climrec  45524  bgoldbtbndlem4  47682  bgoldbtbnd  47683  tgoldbach  47691  2zlidl  47963  2zrngmmgm  47975  lincsumcl  48160