Theorem 3anbi123d 1324

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  1325  3anbi13d  1326  3anbi23d  1327  limeq  4423  smoeq  6375  tfrlemi1  6417  tfr1onlemaccex  6433  tfrcllemaccex  6446  ereq1  6626  updjud  7183  ctssdclemr  7213  tapeq1  7363  tapeq2  7364  elinp  7586  sup3exmid  9029  iccshftr  10115  iccshftl  10117  iccdil  10119  icccntr  10121  fzaddel  10180  elfzomelpfzo  10358  seq3f1olemstep  10657  seq3f1olemp  10658  sumeq1  11608  summodclem2  11635  summodc  11636  zsumdc  11637  prodmodclem2  11830  prodmodc  11831  divalglemnn  12171  divalglemeunn  12174  divalglemeuneg  12176  dfgcd2  12277  pythagtriplem18  12546  pythagtriplem19  12547  ctiunct  12753  ssomct  12758  isstruct2im  12784  isstruct2r  12785  ptex  13038  imasmnd2  13226  imasgrp2  13388  isrngd  13657  imasrng  13660  isringd  13745  imasring  13768  subrngpropd  13920  issubrg3  13951  islmod  13995  lmodlema  13996  islmodd  13997  lmodprop2d  14052  fiinopn  14418  lmfval  14606  upxp  14686  ivthdich  15067  2irrexpqap  15392  dceqnconst  15932  dcapnconst  15933