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  4409  smoeq  6345  tfrlemi1  6387  tfr1onlemaccex  6403  tfrcllemaccex  6416  ereq1  6596  updjud  7143  ctssdclemr  7173  tapeq1  7314  tapeq2  7315  elinp  7536  sup3exmid  8978  iccshftr  10063  iccshftl  10065  iccdil  10067  icccntr  10069  fzaddel  10128  elfzomelpfzo  10301  seq3f1olemstep  10588  seq3f1olemp  10589  sumeq1  11501  summodclem2  11528  summodc  11529  zsumdc  11530  prodmodclem2  11723  prodmodc  11724  divalglemnn  12062  divalglemeunn  12065  divalglemeuneg  12067  dfgcd2  12154  pythagtriplem18  12422  pythagtriplem19  12423  ctiunct  12600  ssomct  12605  isstruct2im  12631  isstruct2r  12632  ptex  12878  imasgrp2  13183  isrngd  13452  imasrng  13455  isringd  13540  imasring  13563  subrngpropd  13715  issubrg3  13746  islmod  13790  lmodlema  13791  islmodd  13792  lmodprop2d  13847  fiinopn  14183  lmfval  14371  upxp  14451  ivthdich  14832  2irrexpqap  15151  dceqnconst  15620  dcapnconst  15621