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  4467  smoeq  6434  tfrlemi1  6476  tfr1onlemaccex  6492  tfrcllemaccex  6505  ereq1  6685  updjud  7245  ctssdclemr  7275  tapeq1  7434  tapeq2  7435  elinp  7657  sup3exmid  9100  iccshftr  10186  iccshftl  10188  iccdil  10190  icccntr  10192  fzaddel  10251  elfzomelpfzo  10432  seq3f1olemstep  10731  seq3f1olemp  10732  wrdl1s1  11158  sumeq1  11861  summodclem2  11888  summodc  11889  zsumdc  11890  prodmodclem2  12083  prodmodc  12084  divalglemnn  12424  divalglemeunn  12427  divalglemeuneg  12429  dfgcd2  12530  pythagtriplem18  12799  pythagtriplem19  12800  ctiunct  13006  ssomct  13011  isstruct2im  13037  isstruct2r  13038  ptex  13292  imasmnd2  13480  imasgrp2  13642  isrngd  13911  imasrng  13914  isringd  13999  imasring  14022  subrngpropd  14174  issubrg3  14205  islmod  14249  lmodlema  14250  islmodd  14251  lmodprop2d  14306  fiinopn  14672  lmfval  14860  upxp  14940  ivthdich  15321  2irrexpqap  15646  wksfval  16028  iswlk  16029  dceqnconst  16387  dcapnconst  16388