Theorem 3anim123d 1471

Description: Deduction joining 3 implications to form implication of conjunctions. (Contributed by NM, 24-Feb-2005.)

Hypotheses

Ref	Expression
3anim123d.1	⊢ (𝜑 → (𝜓 → 𝜒))
3anim123d.2	⊢ (𝜑 → (𝜃 → 𝜏))
3anim123d.3	⊢ (𝜑 → (𝜂 → 𝜁))

Assertion

Ref	Expression
3anim123d	⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) → (𝜒 ∧ 𝜏 ∧ 𝜁)))

Proof of Theorem 3anim123d

Step	Hyp	Ref	Expression
1		3anim123d.1	. . . 4 ⊢ (𝜑 → (𝜓 → 𝜒))
2		3anim123d.2	. . . 4 ⊢ (𝜑 → (𝜃 → 𝜏))
3	1, 2	anim12d 621	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜏)))
4		3anim123d.3	. . 3 ⊢ (𝜑 → (𝜂 → 𝜁))
5	3, 4	anim12d 621	. 2 ⊢ (𝜑 → (((𝜓 ∧ 𝜃) ∧ 𝜂) → ((𝜒 ∧ 𝜏) ∧ 𝜁)))
6		df-3an 1105	. 2 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ ((𝜓 ∧ 𝜃) ∧ 𝜂))
7		df-3an 1105	. 2 ⊢ ((𝜒 ∧ 𝜏 ∧ 𝜁) ↔ ((𝜒 ∧ 𝜏) ∧ 𝜁))
8	5, 6, 7	3imtr4g 299	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) → (𝜒 ∧ 𝜏 ∧ 𝜁)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  pofun  5576  isopolem  7354  mpt3fvot2d  7691  issmo2  8361  smores  8364  inawina  10779  gchina  10788  repswcshw  14968  coprmprod  16842  issubmnd  18959  issubg2  19358  issubrng2  20816  issubrg2  20850  rnglidlmsgrp  21540  rnglidlrng  21541  ocv2ss  21985  issubassa3  22180  sslm  23623  cmetcaulem  25615  bdayfinbndlem1  28859  axcontlem4  29551  axcontlem8  29555  redwlk  30257  subgrpth  30362  clwwlknwwlksn  30635  numclwwlk1lem2foa  30961  dipsubdir  31456  constrconj  34424  onprcf1acwevdlem1  35965  cgr3tr4  36910  idinside  36942  ftc1anclem7  38711  fzmul  38769  fdc1  38774  rngosubdi  38973  rngosubdir  38974  cdlemg33a  41857  grtrimap  49140  grimgrtri  49141  grlimgrtri  49195  upwlkwlk  49331