Theorem 3imp1 1364

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  3an1rs  1376  reupick2  4292  indcardi  10024  ledivge1le  13088  expcan  14204  ltexp2  14205  leexp1a  14210  expnbnd  14267  cshf1  14846  rtrclreclem4  15097  relexpindlem  15099  ncoprmlnprm  16786  rnglidlmcl  21318  xrsdsreclblem  21531  matecl  22550  scmateALT  22637  riinopn  23033  neindisj2  23248  filufint  24045  tsmsxp  24280  ewlkle  29895  uspgr2wlkeq  29935  spthonepeq  30041  wwlksm1edg  30170  clwwisshclwws  30306  clwwlknwwlksn  30329  clwwlkinwwlk  30331  wwlksext2clwwlk  30348  3vfriswmgr  30569  homco1  32093  homulass  32094  hoadddir  32096  satffunlem  35791  mblfinlem3  38197  zerdivemp1x  38485  athgt  40119  psubspi  40410  paddasslem14  40496  eluzge0nn0  47937  iccpartigtl  48060  lighneal  48251  uhgrimisgrgriclem  48583  uhgrimisgrgric  48584  clnbgrgrimlem  48586  uspgrlimlem3  48643  clnbgr3stgrgrlic  48673  gpgusgralem  48709