Theorem 3anbi123d 1349

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

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

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 1007

This theorem is referenced by:  3anbi12d  1350  3anbi13d  1351  3anbi23d  1352  limeq  4480  smoeq  6499  tfrlemi1  6541  tfr1onlemaccex  6557  tfrcllemaccex  6570  ereq1  6752  updjud  7324  ctssdclemr  7354  tapeq1  7514  tapeq2  7515  elinp  7737  sup3exmid  9179  iccshftr  10273  iccshftl  10275  iccdil  10277  icccntr  10279  fzaddel  10339  elfzomelpfzo  10522  seq3f1olemstep  10822  seq3f1olemp  10823  wrdl1s1  11256  sumeq1  11978  summodclem2  12006  summodc  12007  zsumdc  12008  prodmodclem2  12201  prodmodc  12202  divalglemnn  12542  divalglemeunn  12545  divalglemeuneg  12547  dfgcd2  12648  pythagtriplem18  12917  pythagtriplem19  12918  ctiunct  13124  ssomct  13129  isstruct2im  13155  isstruct2r  13156  ptex  13410  imasmnd2  13598  imasgrp2  13760  isrngd  14030  imasrng  14033  isringd  14118  imasring  14141  subrngpropd  14294  issubrg3  14325  islmod  14370  lmodlema  14371  islmodd  14372  lmodprop2d  14427  fiinopn  14798  lmfval  14987  upxp  15066  ivthdich  15447  2irrexpqap  15772  issubgr  16181  wksfval  16246  iswlk  16247  isclwwlk  16318  clwwlkn1loopb  16344  s2elclwwlknon2  16360  3dom  16691  dceqnconst  16776  dcapnconst  16777