Theorem 3imp1 1271

Description: Importation to left triple conjunction. (Contributed by NM, 24-Feb-2005.)

Hypothesis

Ref	Expression
3imp1.1	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Assertion

Ref	Expression
3imp1	⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)

Proof of Theorem 3imp1

Step	Hyp	Ref	Expression
1		3imp1.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
2	1	3imp 1248	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 → 𝜏))
3	2	imp 443	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 382   ∧ w3a 1030

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 195  df-an 384  df-3an 1032

This theorem is referenced by:  reupick2  3871  indcardi  8725  ledivge1le  11736  expcan  12733  ltexp2  12734  leexp1a  12739  expnbnd  12813  cshf1  13356  rtrclreclem4  13598  relexpindlem  13600  ncoprmlnprm  15223  xrsdsreclblem  19560  matecl  19998  scmateALT  20085  riinopn  20486  neindisj2  20685  filufint  21482  tsmsxp  21716  spthonepeq  25911  usg2wlkeq  26030  rusgraprop4  26265  vdn0frgrav2  26344  vdn1frgrav2  26346  usgreghash2spot  26390  homco1  27878  homulass  27879  hoadddir  27881  mblfinlem3  32442  zerdivemp1x  32740  athgt  33584  psubspi  33875  paddasslem14  33961  iccpartigtl  39786  lighneal  39891  eluzge0nn0  40197  ewlkle  40829  uspgr2wlkeq  40876  spthonepeq-av  40980  wwlksm1edg  41100  clwwisshclwws  41257  3vfriswmgr  41470  av-extwwlkfablem2  41532