Theorem 3anbi123d 1312

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

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

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 980

This theorem is referenced by:  3anbi12d  1313  3anbi13d  1314  3anbi23d  1315  limeq  4377  smoeq  6290  tfrlemi1  6332  tfr1onlemaccex  6348  tfrcllemaccex  6361  ereq1  6541  updjud  7080  ctssdclemr  7110  tapeq1  7250  tapeq2  7251  elinp  7472  sup3exmid  8913  iccshftr  9993  iccshftl  9995  iccdil  9997  icccntr  9999  fzaddel  10058  elfzomelpfzo  10230  seq3f1olemstep  10500  seq3f1olemp  10501  sumeq1  11362  summodclem2  11389  summodc  11390  zsumdc  11391  prodmodclem2  11584  prodmodc  11585  divalglemnn  11922  divalglemeunn  11925  divalglemeuneg  11927  dfgcd2  12014  pythagtriplem18  12280  pythagtriplem19  12281  ctiunct  12440  ssomct  12445  isstruct2im  12471  isstruct2r  12472  ptex  12712  isringd  13218  issubrg3  13373  fiinopn  13440  lmfval  13628  upxp  13708  2irrexpqap  14332  dceqnconst  14743  dcapnconst  14744