Theorem 3anbi123d 1323

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

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

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 982

This theorem is referenced by:  3anbi12d  1324  3anbi13d  1325  3anbi23d  1326  limeq  4413  smoeq  6357  tfrlemi1  6399  tfr1onlemaccex  6415  tfrcllemaccex  6428  ereq1  6608  updjud  7157  ctssdclemr  7187  tapeq1  7335  tapeq2  7336  elinp  7558  sup3exmid  9001  iccshftr  10086  iccshftl  10088  iccdil  10090  icccntr  10092  fzaddel  10151  elfzomelpfzo  10324  seq3f1olemstep  10623  seq3f1olemp  10624  sumeq1  11537  summodclem2  11564  summodc  11565  zsumdc  11566  prodmodclem2  11759  prodmodc  11760  divalglemnn  12100  divalglemeunn  12103  divalglemeuneg  12105  dfgcd2  12206  pythagtriplem18  12475  pythagtriplem19  12476  ctiunct  12682  ssomct  12687  isstruct2im  12713  isstruct2r  12714  ptex  12966  imasmnd2  13154  imasgrp2  13316  isrngd  13585  imasrng  13588  isringd  13673  imasring  13696  subrngpropd  13848  issubrg3  13879  islmod  13923  lmodlema  13924  islmodd  13925  lmodprop2d  13980  fiinopn  14324  lmfval  14512  upxp  14592  ivthdich  14973  2irrexpqap  15298  dceqnconst  15791  dcapnconst  15792