Theorem 3anbi123d 1349

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 473	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜏)))
4		bi3d.3	. . 3 ⊢ (𝜑 → (𝜂 ↔ 𝜁))
5	3, 4	anbi12d 473	. 2 ⊢ (𝜑 → (((𝜓 ∧ 𝜃) ∧ 𝜂) ↔ ((𝜒 ∧ 𝜏) ∧ 𝜁)))
6		df-3an 1007	. 2 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ ((𝜓 ∧ 𝜃) ∧ 𝜂))
7		df-3an 1007	. 2 ⊢ ((𝜒 ∧ 𝜏 ∧ 𝜁) ↔ ((𝜒 ∧ 𝜏) ∧ 𝜁))
8	5, 6, 7	3bitr4g 223	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜁)))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∧ w3a 1005

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1007

This theorem is referenced by:  3anbi12d  1350  3anbi13d  1351  3anbi23d  1352  limeq  4498  smoeq  6521  tfrlemi1  6563  tfr1onlemaccex  6579  tfrcllemaccex  6592  ereq1  6774  updjud  7373  ctssdclemr  7403  tapeq1  7566  tapeq2  7567  elinp  7789  sup3exmid  9231  iccshftr  10327  iccshftl  10329  iccdil  10331  icccntr  10333  fzaddel  10393  elfzomelpfzo  10576  seq3f1olemstep  10876  seq3f1olemp  10877  wrdl1s1  11318  sumeq1  12040  summodclem2  12068  summodc  12069  zsumdc  12070  prodmodclem2  12263  prodmodc  12264  divalglemnn  12604  divalglemeunn  12607  divalglemeuneg  12609  dfgcd2  12710  pythagtriplem18  12979  pythagtriplem19  12980  ctiunct  13191  ssomct  13196  isstruct2im  13222  isstruct2r  13223  ptex  13477  imasmnd2  13665  imasgrp2  13827  isrngd  14097  imasrng  14100  isringd  14185  imasring  14208  subrngpropd  14361  issubrg3  14392  islmod  14439  lmodlema  14440  islmodd  14441  lmodprop2d  14496  fiinopn  14869  lmfval  15058  upxp  15137  ivthdich  15518  2irrexpqap  15843  issubgr  16252  wksfval  16317  iswlk  16318  isclwwlk  16389  clwwlkn1loopb  16415  s2elclwwlknon2  16431  3dom  16762  dceqnconst  16846  dcapnconst  16847