Theorem exp41 636

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  ad5ant2345  1309  tz7.49  7427  supxrun  12018  injresinj  12451  fi1uzind  13134  brfi1indALT  13137  fi1uzindOLD  13140  brfi1indALTOLD  13143  swrdswrdlem  13311  swrdswrd  13312  2cshwcshw  13422  cshwcsh2id  13425  prmgaplem6  15598  cusgrasize2inds  26005  usgra2adedgwlkonALT  26144  usgra2wlkspthlem2  26148  3v3e3cycl1  26172  constr3cycl  26189  4cycl4v4e  26194  4cycl4dv4e  26196  wwlknext  26252  wwlkextproplem3  26271  clwlkisclwwlklem2a4  26312  clwlkisclwwlklem1  26315  usghashecclwwlk  26362  clwlkfclwwlk  26371  el2wlkonot  26396  2spontn0vne  26414  rusgranumwlks  26483  1to3vfriswmgra  26534  frgranbnb  26547  frgrawopreg  26576  usg2spot2nb  26592  extwwlkfablem2  26605  numclwwlkovf2ex  26613  branmfn  28348  relowlpssretop  32388  broucube  32613  eel0001  37966  eel0000  37967  eel1111  37968  eel00001  37969  eel00000  37970  eel11111  37971  climrec  38670  bgoldbtbndlem4  40224  bgoldbtbnd  40225  tgoldbach  40232  tgoldbachOLD  40239  cusgrsize2inds  40669  usgr2pthlem  40969  usgr2pth  40970  wwlksnext  41099  elwwlks2  41170  rusgrnumwwlks  41177  clwlkclwwlklem2a4  41206  clwlkclwwlklem2  41209  umgrhashecclwwlk  41262  clwlksfclwwlk  41269  1to3vfriswmgr  41450  frgrnbnb  41463  frgrwopreg  41486  av-numclwwlkovf2ex  41517  2zlidl  41724  2zrngmmgm  41736  lincsumcl  42014