Theorem 3anbi123d 1353

Description: Deduction joining 3 equivalences to form equivalence of conjunctions. (Contributed by NM, 22-Apr-1994.)

Hypotheses

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

Assertion

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

Proof of Theorem 3anbi123d

Step	Hyp	Ref	Expression
1		bi3d.1	. . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		bi3d.2	. . . 4 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
3	1, 2	anbi12d 477	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜏)))
4		bi3d.3	. . 3 ⊢ (𝜑 → (𝜂 ↔ 𝜁))
5	3, 4	anbi12d 477	. 2 ⊢ (𝜑 → (((𝜓 ∧ 𝜃) ∧ 𝜂) ↔ ((𝜒 ∧ 𝜏) ∧ 𝜁)))
6		df-3an 1011	. 2 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ ((𝜓 ∧ 𝜃) ∧ 𝜂))
7		df-3an 1011	. 2 ⊢ ((𝜒 ∧ 𝜏 ∧ 𝜁) ↔ ((𝜒 ∧ 𝜏) ∧ 𝜁))
8	5, 6, 7	3bitr4g 223	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜁)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  3anbi12d  1354  3anbi13d  1355  3anbi23d  1356  limeq  4522  smoeq  6561  tfrlemi1  6603  tfr1onlemaccex  6619  tfrcllemaccex  6632  ereq1  6814  updjud  7422  ctssdclemr  7452  tapeq1  7618  tapeq2  7619  elinp  7841  sup3exmid  9289  iccshftr  10406  iccshftl  10408  iccdil  10410  icccntr  10412  fzaddel  10475  elfzomelpfzo  10659  seq3f1olemstep  10964  seq3f1olemp  10965  wrdl1s1  11412  sumeq1  12137  summodclem2  12165  summodc  12166  zsumdc  12167  prodmodclem2  12360  prodmodc  12361  divalglemnn  12701  divalglemeunn  12704  divalglemeuneg  12706  dfgcd2  12807  pythagtriplem18  13080  pythagtriplem19  13081  ctiunct  13380  ssomct  13385  isstruct2im  13411  isstruct2r  13412  ptex  13667  imasmnd2  13808  imasgrp2  13962  isrngd  14301  imasrng  14304  isringd  14395  imasring  14418  subrngpropd  14573  issubrg3  14604  islmod  14676  lmodlema  14677  islmodd  14678  lmodprop2d  14734  fiinopn  15154  lmfval  15343  upxp  15422  ivthdich  15803  2irrexpqap  16133  issubgr  16596  wksfval  16661  iswlk  16662  isclwwlk  16733  clwwlkn1loopb  16759  s2elclwwlknon2  16775  3dom  17116  dceqnconst  17208  dcapnconst  17209