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  8485  supxrun  13358  injresinj  13827  fi1uzind  14546  brfi1indALT  14549  swrdswrdlem  14742  swrdswrd  14743  2cshwcshw  14864  cshwcsh2id  14867  prmgaplem6  17094  cusgrsize2inds  29471  usgr2pthlem  29783  usgr2pth  29784  elwwlks2  29986  rusgrnumwwlks  29994  clwlkclwwlklem2a4  30016  clwlkclwwlklem2  30019  umgrhashecclwwlk  30097  1to3vfriswmgr  30299  frgrnbnb  30312  branmfn  32124  elrspunidl  33456  dfufd2lem  33577  zarcmplem  33880  relowlpssretop  37365  broucube  37661  eel0000  44740  eel00001  44741  eel00000  44742  eel11111  44743  climrec  45618  bgoldbtbndlem4  47795  bgoldbtbnd  47796  tgoldbach  47804  2zlidl  48156  2zrngmmgm  48168  lincsumcl  48348