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  5581  isopolem  7346  issmo2  8338  smores  8341  inawina  10699  gchina  10708  repswcshw  14883  coprmprod  16751  issubmnd  18866  issubg2  19265  issubrng2  20720  issubrg2  20754  rnglidlmsgrp  21443  rnglidlrng  21444  ocv2ss  21886  issubassa3  22081  sslm  23524  cmetcaulem  25516  bdayfinbndlem1  28732  axcontlem4  29424  axcontlem8  29428  redwlk  30130  subgrpth  30235  clwwlknwwlksn  30508  numclwwlk1lem2foa  30834  dipsubdir  31329  constrconj  34255  cgr3tr4  36632  idinside  36664  ftc1anclem7  38448  fzmul  38491  fdc1  38496  rngosubdi  38695  rngosubdir  38696  cdlemg33a  41579  grtrimap  48864  grimgrtri  48865  grlimgrtri  48919  upwlkwlk  49055