Theorem exp41 437

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 415	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → (𝜃 → 𝜏))
3	2	exp31 422	1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  ad5ant2345  1366  tz7.49  8083  supxrun  12712  injresinj  13161  fi1uzind  13858  brfi1indALT  13861  swrdswrdlem  14068  swrdswrd  14069  2cshwcshw  14189  cshwcsh2id  14192  prmgaplem6  16394  cusgrsize2inds  27237  usgr2pthlem  27546  usgr2pth  27547  elwwlks2  27747  rusgrnumwwlks  27755  clwlkclwwlklem2a4  27777  clwlkclwwlklem2  27780  umgrhashecclwwlk  27859  1to3vfriswmgr  28061  frgrnbnb  28074  branmfn  29884  relowlpssretop  34647  broucube  34928  eel0000  41061  eel00001  41062  eel00000  41063  eel11111  41064  climrec  41891  bgoldbtbndlem4  43980  bgoldbtbnd  43981  tgoldbach  43989  isomuspgr  44006  2zlidl  44212  2zrngmmgm  44224  lincsumcl  44493