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  4413  smoeq  6357  tfrlemi1  6399  tfr1onlemaccex  6415  tfrcllemaccex  6428  ereq1  6608  updjud  7157  ctssdclemr  7187  tapeq1  7337  tapeq2  7338  elinp  7560  sup3exmid  9003  iccshftr  10088  iccshftl  10090  iccdil  10092  icccntr  10094  fzaddel  10153  elfzomelpfzo  10326  seq3f1olemstep  10625  seq3f1olemp  10626  sumeq1  11539  summodclem2  11566  summodc  11567  zsumdc  11568  prodmodclem2  11761  prodmodc  11762  divalglemnn  12102  divalglemeunn  12105  divalglemeuneg  12107  dfgcd2  12208  pythagtriplem18  12477  pythagtriplem19  12478  ctiunct  12684  ssomct  12689  isstruct2im  12715  isstruct2r  12716  ptex  12968  imasmnd2  13156  imasgrp2  13318  isrngd  13587  imasrng  13590  isringd  13675  imasring  13698  subrngpropd  13850  issubrg3  13881  islmod  13925  lmodlema  13926  islmodd  13927  lmodprop2d  13982  fiinopn  14348  lmfval  14536  upxp  14616  ivthdich  14997  2irrexpqap  15322  dceqnconst  15817  dcapnconst  15818