Theorem 3anbi123d 1346

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

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

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 1004

This theorem is referenced by:  3anbi12d  1347  3anbi13d  1348  3anbi23d  1349  limeq  4472  smoeq  6451  tfrlemi1  6493  tfr1onlemaccex  6509  tfrcllemaccex  6522  ereq1  6704  updjud  7272  ctssdclemr  7302  tapeq1  7461  tapeq2  7462  elinp  7684  sup3exmid  9127  iccshftr  10219  iccshftl  10221  iccdil  10223  icccntr  10225  fzaddel  10284  elfzomelpfzo  10466  seq3f1olemstep  10766  seq3f1olemp  10767  wrdl1s1  11197  sumeq1  11906  summodclem2  11933  summodc  11934  zsumdc  11935  prodmodclem2  12128  prodmodc  12129  divalglemnn  12469  divalglemeunn  12472  divalglemeuneg  12474  dfgcd2  12575  pythagtriplem18  12844  pythagtriplem19  12845  ctiunct  13051  ssomct  13056  isstruct2im  13082  isstruct2r  13083  ptex  13337  imasmnd2  13525  imasgrp2  13687  isrngd  13956  imasrng  13959  isringd  14044  imasring  14067  subrngpropd  14220  issubrg3  14251  islmod  14295  lmodlema  14296  islmodd  14297  lmodprop2d  14352  fiinopn  14718  lmfval  14907  upxp  14986  ivthdich  15367  2irrexpqap  15692  wksfval  16119  iswlk  16120  isclwwlk  16189  clwwlkn1loopb  16215  s2elclwwlknon2  16231  3dom  16523  dceqnconst  16600  dcapnconst  16601