Theorem exp41 434

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  ad5ant2345  1372  tz7.49  8373  supxrun  13222  injresinj  13698  fi1uzind  14421  brfi1indALT  14424  swrdswrdlem  14618  swrdswrd  14619  2cshwcshw  14739  cshwcsh2id  14742  prmgaplem6  16975  cusgrsize2inds  29453  usgr2pthlem  29762  usgr2pth  29763  elwwlks2  29968  rusgrnumwwlks  29976  clwlkclwwlklem2a4  29998  clwlkclwwlklem2  30001  umgrhashecclwwlk  30079  1to3vfriswmgr  30281  frgrnbnb  30294  branmfn  32106  elrspunidl  33437  dfufd2lem  33558  zarcmplem  33966  relowlpssretop  37481  broucube  37767  eel0000  44876  eel00001  44877  eel00000  44878  eel11111  44879  climrec  45765  bgoldbtbndlem4  47970  bgoldbtbnd  47971  tgoldbach  47979  2zlidl  48402  2zrngmmgm  48414  lincsumcl  48593