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  4422  smoeq  6366  tfrlemi1  6408  tfr1onlemaccex  6424  tfrcllemaccex  6437  ereq1  6617  updjud  7166  ctssdclemr  7196  tapeq1  7346  tapeq2  7347  elinp  7569  sup3exmid  9012  iccshftr  10098  iccshftl  10100  iccdil  10102  icccntr  10104  fzaddel  10163  elfzomelpfzo  10341  seq3f1olemstep  10640  seq3f1olemp  10641  sumeq1  11585  summodclem2  11612  summodc  11613  zsumdc  11614  prodmodclem2  11807  prodmodc  11808  divalglemnn  12148  divalglemeunn  12151  divalglemeuneg  12153  dfgcd2  12254  pythagtriplem18  12523  pythagtriplem19  12524  ctiunct  12730  ssomct  12735  isstruct2im  12761  isstruct2r  12762  ptex  13014  imasmnd2  13202  imasgrp2  13364  isrngd  13633  imasrng  13636  isringd  13721  imasring  13744  subrngpropd  13896  issubrg3  13927  islmod  13971  lmodlema  13972  islmodd  13973  lmodprop2d  14028  fiinopn  14394  lmfval  14582  upxp  14662  ivthdich  15043  2irrexpqap  15368  dceqnconst  15863  dcapnconst  15864