Theorem exp41 438

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  ad5ant2345  1371  tz7.49  8122  supxrun  12804  injresinj  13261  fi1uzind  13961  brfi1indALT  13964  swrdswrdlem  14167  swrdswrd  14168  2cshwcshw  14288  cshwcsh2id  14291  prmgaplem6  16504  cusgrsize2inds  27407  usgr2pthlem  27716  usgr2pth  27717  elwwlks2  27916  rusgrnumwwlks  27924  clwlkclwwlklem2a4  27946  clwlkclwwlklem2  27949  umgrhashecclwwlk  28027  1to3vfriswmgr  28229  frgrnbnb  28242  branmfn  30052  elrspunidl  31190  zarcmplem  31415  relowlpssretop  35190  broucube  35466  eel0000  41918  eel00001  41919  eel00000  41920  eel11111  41921  climrec  42726  bgoldbtbndlem4  44841  bgoldbtbnd  44842  tgoldbach  44850  isomuspgr  44867  2zlidl  45073  2zrngmmgm  45085  lincsumcl  45353