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  4379  smoeq  6293  tfrlemi1  6335  tfr1onlemaccex  6351  tfrcllemaccex  6364  ereq1  6544  updjud  7083  ctssdclemr  7113  tapeq1  7253  tapeq2  7254  elinp  7475  sup3exmid  8916  iccshftr  9996  iccshftl  9998  iccdil  10000  icccntr  10002  fzaddel  10061  elfzomelpfzo  10233  seq3f1olemstep  10503  seq3f1olemp  10504  sumeq1  11365  summodclem2  11392  summodc  11393  zsumdc  11394  prodmodclem2  11587  prodmodc  11588  divalglemnn  11925  divalglemeunn  11928  divalglemeuneg  11930  dfgcd2  12017  pythagtriplem18  12283  pythagtriplem19  12284  ctiunct  12443  ssomct  12448  isstruct2im  12474  isstruct2r  12475  ptex  12718  isringd  13225  issubrg3  13373  islmod  13386  lmodlema  13387  islmodd  13388  lmodprop2d  13443  fiinopn  13589  lmfval  13777  upxp  13857  2irrexpqap  14481  dceqnconst  14893  dcapnconst  14894