Theorem 3anbi123d 1348

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

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

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 1006

This theorem is referenced by:  3anbi12d  1349  3anbi13d  1350  3anbi23d  1351  limeq  4474  smoeq  6456  tfrlemi1  6498  tfr1onlemaccex  6514  tfrcllemaccex  6527  ereq1  6709  updjud  7281  ctssdclemr  7311  tapeq1  7471  tapeq2  7472  elinp  7694  sup3exmid  9137  iccshftr  10229  iccshftl  10231  iccdil  10233  icccntr  10235  fzaddel  10294  elfzomelpfzo  10477  seq3f1olemstep  10777  seq3f1olemp  10778  wrdl1s1  11208  sumeq1  11917  summodclem2  11945  summodc  11946  zsumdc  11947  prodmodclem2  12140  prodmodc  12141  divalglemnn  12481  divalglemeunn  12484  divalglemeuneg  12486  dfgcd2  12587  pythagtriplem18  12856  pythagtriplem19  12857  ctiunct  13063  ssomct  13068  isstruct2im  13094  isstruct2r  13095  ptex  13349  imasmnd2  13537  imasgrp2  13699  isrngd  13969  imasrng  13972  isringd  14057  imasring  14080  subrngpropd  14233  issubrg3  14264  islmod  14308  lmodlema  14309  islmodd  14310  lmodprop2d  14365  fiinopn  14731  lmfval  14920  upxp  14999  ivthdich  15380  2irrexpqap  15705  issubgr  16111  wksfval  16176  iswlk  16177  isclwwlk  16248  clwwlkn1loopb  16274  s2elclwwlknon2  16290  3dom  16608  dceqnconst  16685  dcapnconst  16686