Theorem 3anim123d 1472

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  5584  isopolem  7384  mpt3fvot2d  7722  issmo2  8395  smores  8398  inawina  10814  gchina  10823  repswcshw  15005  coprmprod  16880  issubmnd  19003  issubg2  19402  issubrng2  20861  issubrg2  20895  rnglidlmsgrp  21585  rnglidlrng  21586  ocv2ss  22034  issubassa3  22229  sslm  23672  cmetcaulem  25664  bdayfinbndlem1  28910  axcontlem4  29602  axcontlem8  29606  redwlk  30308  subgrpth  30413  clwwlknwwlksn  30686  numclwwlk1lem2foa  31012  dipsubdir  31507  constrconj  34488  onprcf1acwevdlem1  36086  cgr3tr4  37032  idinside  37064  ftc1anclem7  38885  fzmul  38941  fdc1  38946  rngosubdi  39145  rngosubdir  39146  cdlemg33a  42029  grtrimap  49319  grimgrtri  49320  grlimgrtri  49374  upwlkwlk  49510