Theorem 3anbi123d 1325

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

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

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 983

This theorem is referenced by:  3anbi12d  1326  3anbi13d  1327  3anbi23d  1328  limeq  4432  smoeq  6389  tfrlemi1  6431  tfr1onlemaccex  6447  tfrcllemaccex  6460  ereq1  6640  updjud  7199  ctssdclemr  7229  tapeq1  7384  tapeq2  7385  elinp  7607  sup3exmid  9050  iccshftr  10136  iccshftl  10138  iccdil  10140  icccntr  10142  fzaddel  10201  elfzomelpfzo  10382  seq3f1olemstep  10681  seq3f1olemp  10682  wrdl1s1  11107  sumeq1  11741  summodclem2  11768  summodc  11769  zsumdc  11770  prodmodclem2  11963  prodmodc  11964  divalglemnn  12304  divalglemeunn  12307  divalglemeuneg  12309  dfgcd2  12410  pythagtriplem18  12679  pythagtriplem19  12680  ctiunct  12886  ssomct  12891  isstruct2im  12917  isstruct2r  12918  ptex  13171  imasmnd2  13359  imasgrp2  13521  isrngd  13790  imasrng  13793  isringd  13878  imasring  13901  subrngpropd  14053  issubrg3  14084  islmod  14128  lmodlema  14129  islmodd  14130  lmodprop2d  14185  fiinopn  14551  lmfval  14739  upxp  14819  ivthdich  15200  2irrexpqap  15525  dceqnconst  16140  dcapnconst  16141