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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  3an1rs  1360  reupick2  4321  indcardi  10036  ledivge1le  13045  expcan  14134  ltexp2  14135  leexp1a  14140  expnbnd  14195  cshf1  14760  rtrclreclem4  15008  relexpindlem  15010  ncoprmlnprm  16664  xrsdsreclblem  20991  matecl  21927  scmateALT  22014  riinopn  22410  neindisj2  22627  filufint  23424  tsmsxp  23659  ewlkle  28862  uspgr2wlkeq  28903  spthonepeq  29009  wwlksm1edg  29135  clwwisshclwws  29268  clwwlknwwlksn  29291  clwwlkinwwlk  29293  wwlksext2clwwlk  29310  3vfriswmgr  29531  homco1  31054  homulass  31055  hoadddir  31057  satffunlem  34392  mblfinlem3  36527  zerdivemp1x  36815  athgt  38327  psubspi  38618  paddasslem14  38704  eluzge0nn0  46020  iccpartigtl  46091  lighneal  46279  isomgrsym  46504  rnglidlmcl  46748