Theorem exp41 426

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

Syntax hints:   → wi 4   ∧ wa 385

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 199  df-an 386

This theorem is referenced by:  syl1111anc  869  ad5ant2345  1490  tz7.49  7780  supxrun  12394  injresinj  12843  fi1uzind  13527  brfi1indALT  13530  swrdswrdlem  13746  swrdswrd  13747  2cshwcshw  13909  cshwcsh2id  13912  prmgaplem6  16092  cusgrsize2inds  26702  usgr2pthlem  27016  usgr2pth  27017  wwlksnext  27161  elwwlks2  27256  rusgrnumwwlks  27264  rusgrnumwwlksOLD  27265  clwlkclwwlklem2a4  27289  clwlkclwwlklem2  27292  umgrhashecclwwlk  27395  clwlksfclwwlkOLD  27402  1to3vfriswmgr  27628  frgrnbnb  27641  branmfn  29488  relowlpssretop  33709  broucube  33931  eel0001  39710  eel0000  39711  eel00001  39712  eel00000  39713  eel11111  39714  climrec  40574  bgoldbtbndlem4  42473  bgoldbtbnd  42474  tgoldbach  42482  isomuspgr  42499  2zlidl  42728  2zrngmmgm  42740  lincsumcl  43014