Theorem 3imp1 1348

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 1110	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 → 𝜏))
3	2	imp 406	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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  df-3an 1088

This theorem is referenced by:  3an1rs  1360  reupick2  4294  indcardi  9994  ledivge1le  13024  expcan  14134  ltexp2  14135  leexp1a  14140  expnbnd  14197  cshf1  14775  rtrclreclem4  15027  relexpindlem  15029  ncoprmlnprm  16698  rnglidlmcl  21126  xrsdsreclblem  21329  matecl  22312  scmateALT  22399  riinopn  22795  neindisj2  23010  filufint  23807  tsmsxp  24042  ewlkle  29533  uspgr2wlkeq  29574  spthonepeq  29682  wwlksm1edg  29811  clwwisshclwws  29944  clwwlknwwlksn  29967  clwwlkinwwlk  29969  wwlksext2clwwlk  29986  3vfriswmgr  30207  homco1  31730  homulass  31731  hoadddir  31733  satffunlem  35388  mblfinlem3  37653  zerdivemp1x  37941  athgt  39450  psubspi  39741  paddasslem14  39827  eluzge0nn0  47313  iccpartigtl  47424  lighneal  47612  uhgrimisgrgriclem  47930  uhgrimisgrgric  47931  clnbgrgrimlem  47933  uspgrlimlem3  47989  clnbgr3stgrgrlic  48011  gpgusgralem  48047