Theorem exp41 638

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

Syntax hints:   → wi 4   ∧ wa 384

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

This theorem is referenced by:  ad5ant2345  1317  tz7.49  7540  supxrun  12146  injresinj  12589  fi1uzind  13279  brfi1indALT  13282  fi1uzindOLD  13285  brfi1indALTOLD  13288  swrdswrdlem  13459  swrdswrd  13460  2cshwcshw  13571  cshwcsh2id  13574  prmgaplem6  15760  cusgrsize2inds  26349  usgr2pthlem  26659  usgr2pth  26660  wwlksnext  26788  elwwlks2  26861  rusgrnumwwlks  26869  clwlkclwwlklem2a4  26898  clwlkclwwlklem2  26901  umgrhashecclwwlk  26955  clwlksfclwwlk  26962  1to3vfriswmgr  27144  frgrnbnb  27157  branmfn  28964  relowlpssretop  33212  broucube  33443  eel0001  38945  eel0000  38946  eel1111  38947  eel00001  38948  eel00000  38949  eel11111  38950  climrec  39835  bgoldbtbndlem4  41696  bgoldbtbnd  41697  tgoldbach  41705  tgoldbachOLD  41712  2zlidl  41934  2zrngmmgm  41946  lincsumcl  42220