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  6455  tfrlemi1  6497  tfr1onlemaccex  6513  tfrcllemaccex  6526  ereq1  6708  updjud  7280  ctssdclemr  7310  tapeq1  7470  tapeq2  7471  elinp  7693  sup3exmid  9136  iccshftr  10228  iccshftl  10230  iccdil  10232  icccntr  10234  fzaddel  10293  elfzomelpfzo  10475  seq3f1olemstep  10775  seq3f1olemp  10776  wrdl1s1  11206  sumeq1  11915  summodclem2  11942  summodc  11943  zsumdc  11944  prodmodclem2  12137  prodmodc  12138  divalglemnn  12478  divalglemeunn  12481  divalglemeuneg  12483  dfgcd2  12584  pythagtriplem18  12853  pythagtriplem19  12854  ctiunct  13060  ssomct  13065  isstruct2im  13091  isstruct2r  13092  ptex  13346  imasmnd2  13534  imasgrp2  13696  isrngd  13965  imasrng  13968  isringd  14053  imasring  14076  subrngpropd  14229  issubrg3  14260  islmod  14304  lmodlema  14305  islmodd  14306  lmodprop2d  14361  fiinopn  14727  lmfval  14916  upxp  14995  ivthdich  15376  2irrexpqap  15701  issubgr  16107  wksfval  16172  iswlk  16173  isclwwlk  16244  clwwlkn1loopb  16270  s2elclwwlknon2  16286  3dom  16587  dceqnconst  16664  dcapnconst  16665