Theorem 3imp1 1343

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  3an1rs  1355  reupick2  4288  indcardi  9466  ledivge1le  12459  expcan  13532  ltexp2  13533  leexp1a  13538  expnbnd  13592  cshf1  14171  rtrclreclem4  14419  relexpindlem  14421  ncoprmlnprm  16067  xrsdsreclblem  20590  matecl  21033  scmateALT  21120  riinopn  21515  neindisj2  21730  filufint  22527  tsmsxp  22762  ewlkle  27386  uspgr2wlkeq  27426  spthonepeq  27532  wwlksm1edg  27658  clwwisshclwws  27792  clwwlknwwlksn  27815  clwwlkinwwlk  27817  wwlksext2clwwlk  27835  3vfriswmgr  28056  homco1  29577  homulass  29578  hoadddir  29580  satffunlem  32648  mblfinlem3  34930  zerdivemp1x  35224  athgt  36591  psubspi  36882  paddasslem14  36968  eluzge0nn0  43511  iccpartigtl  43582  lighneal  43775  isomgrsym  44000