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  8386  supxrun  13243  injresinj  13719  fi1uzind  14442  brfi1indALT  14445  swrdswrdlem  14639  swrdswrd  14640  2cshwcshw  14760  cshwcsh2id  14763  prmgaplem6  16996  cusgrsize2inds  29539  usgr2pthlem  29848  usgr2pth  29849  elwwlks2  30054  rusgrnumwwlks  30062  clwlkclwwlklem2a4  30084  clwlkclwwlklem2  30087  umgrhashecclwwlk  30165  1to3vfriswmgr  30367  frgrnbnb  30380  branmfn  32193  elrspunidl  33521  dfufd2lem  33642  zarcmplem  34059  relowlpssretop  37619  broucube  37905  eel0000  45075  eel00001  45076  eel00000  45077  eel11111  45078  climrec  45963  bgoldbtbndlem4  48168  bgoldbtbnd  48169  tgoldbach  48177  2zlidl  48600  2zrngmmgm  48612  lincsumcl  48791