Theorem 3anbi123d 1323

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  1324  3anbi13d  1325  3anbi23d  1326  limeq  4412  smoeq  6348  tfrlemi1  6390  tfr1onlemaccex  6406  tfrcllemaccex  6419  ereq1  6599  updjud  7148  ctssdclemr  7178  tapeq1  7319  tapeq2  7320  elinp  7541  sup3exmid  8984  iccshftr  10069  iccshftl  10071  iccdil  10073  icccntr  10075  fzaddel  10134  elfzomelpfzo  10307  seq3f1olemstep  10606  seq3f1olemp  10607  sumeq1  11520  summodclem2  11547  summodc  11548  zsumdc  11549  prodmodclem2  11742  prodmodc  11743  divalglemnn  12083  divalglemeunn  12086  divalglemeuneg  12088  dfgcd2  12181  pythagtriplem18  12450  pythagtriplem19  12451  ctiunct  12657  ssomct  12662  isstruct2im  12688  isstruct2r  12689  ptex  12935  imasgrp2  13240  isrngd  13509  imasrng  13512  isringd  13597  imasring  13620  subrngpropd  13772  issubrg3  13803  islmod  13847  lmodlema  13848  islmodd  13849  lmodprop2d  13904  fiinopn  14240  lmfval  14428  upxp  14508  ivthdich  14889  2irrexpqap  15214  dceqnconst  15704  dcapnconst  15705