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

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

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 1089

This theorem is referenced by:  3an1rs  1360  reupick2  4331  indcardi  10081  ledivge1le  13106  expcan  14209  ltexp2  14210  leexp1a  14215  expnbnd  14271  cshf1  14848  rtrclreclem4  15100  relexpindlem  15102  ncoprmlnprm  16765  rnglidlmcl  21226  xrsdsreclblem  21430  matecl  22431  scmateALT  22518  riinopn  22914  neindisj2  23131  filufint  23928  tsmsxp  24163  ewlkle  29623  uspgr2wlkeq  29664  spthonepeq  29772  wwlksm1edg  29901  clwwisshclwws  30034  clwwlknwwlksn  30057  clwwlkinwwlk  30059  wwlksext2clwwlk  30076  3vfriswmgr  30297  homco1  31820  homulass  31821  hoadddir  31823  satffunlem  35406  mblfinlem3  37666  zerdivemp1x  37954  athgt  39458  psubspi  39749  paddasslem14  39835  eluzge0nn0  47324  iccpartigtl  47410  lighneal  47598  uhgrimisgrgriclem  47898  uhgrimisgrgric  47899  clnbgrgrimlem  47901  uspgrlimlem3  47957  clnbgr3stgrgrlic  47979  gpgusgralem  48011