Theorem 3imp1 1409

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

Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1071

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 199  df-an 387  df-3an 1073

This theorem is referenced by:  3an1rs  1421  reupick2  4139  indcardi  9199  ledivge1le  12214  expcan  13235  ltexp2  13236  leexp1a  13241  expnbnd  13316  cshf1  13965  rtrclreclem4  14212  relexpindlem  14214  ncoprmlnprm  15844  xrsdsreclblem  20192  matecl  20639  scmateALT  20727  riinopn  21124  neindisj2  21339  filufint  22136  tsmsxp  22370  ewlkle  26957  uspgr2wlkeq  26997  spthonepeq  27108  wwlksm1edg  27234  wwlksm1edgOLD  27235  clwwisshclwws  27408  clwwlknwwlksn  27431  clwwlkinwwlk  27433  clwwlkinwwlkOLD  27434  wwlksext2clwwlk  27458  3vfriswmgr  27690  homco1  29236  homulass  29237  hoadddir  29239  mblfinlem3  34079  zerdivemp1x  34375  athgt  35615  psubspi  35906  paddasslem14  35992  eluzge0nn0  42364  iccpartigtl  42401  lighneal  42559  isomgrsym  42759