Theorem 3anim123d 1467

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 620	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜏)))
4		3anim123d.3	. . 3 ⊢ (𝜑 → (𝜂 → 𝜁))
5	3, 4	anim12d 620	. 2 ⊢ (𝜑 → (((𝜓 ∧ 𝜃) ∧ 𝜂) → ((𝜒 ∧ 𝜏) ∧ 𝜁)))
6		df-3an 1103	. 2 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ ((𝜓 ∧ 𝜃) ∧ 𝜂))
7		df-3an 1103	. 2 ⊢ ((𝜒 ∧ 𝜏 ∧ 𝜁) ↔ ((𝜒 ∧ 𝜏) ∧ 𝜁))
8	5, 6, 7	3imtr4g 299	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:  pofun  5577  isopolem  7333  issmo2  8324  smores  8327  inawina  10663  gchina  10672  repswcshw  14837  coprmprod  16707  issubmnd  18807  issubg2  19196  issubrng2  20631  issubrg2  20665  rnglidlmsgrp  21342  rnglidlrng  21343  ocv2ss  21780  issubassa3  21973  sslm  23413  cmetcaulem  25404  bdayfinbndlem1  28614  axcontlem4  29222  axcontlem8  29226  redwlk  29925  clwwlknwwlksn  30294  numclwwlk1lem2foa  30610  dipsubdir  31105  constrconj  34047  subgrpth  35492  cgr3tr4  36410  idinside  36442  ftc1anclem7  38205  fzmul  38247  fdc1  38252  rngosubdi  38451  rngosubdir  38452  cdlemg33a  41337  grtrimap  48569  grimgrtri  48570  grlimgrtri  48624  upwlkwlk  48760