Theorem 3anbi23d 1441

Description: Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.)

Hypotheses

Ref	Expression
3anbi12d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
3anbi12d.2	⊢ (𝜑 → (𝜃 ↔ 𝜏))

Assertion

Ref	Expression
3anbi23d	⊢ (𝜑 → ((𝜂 ∧ 𝜓 ∧ 𝜃) ↔ (𝜂 ∧ 𝜒 ∧ 𝜏)))

Proof of Theorem 3anbi23d

Step	Hyp	Ref	Expression
1		biidd 262	. 2 ⊢ (𝜑 → (𝜂 ↔ 𝜂))
2		3anbi12d.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3		3anbi12d.2	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	1, 2, 3	3anbi123d 1438	1 ⊢ (𝜑 → ((𝜂 ∧ 𝜓 ∧ 𝜃) ↔ (𝜂 ∧ 𝜒 ∧ 𝜏)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088

This theorem is referenced by:  f1dom3el3dif  7246  xpord2lem  8123  xpord3lem  8130  frecseq123  8263  oeeui  8568  sbthfi  9168  pwfseqlem4a  10620  pwfseqlem4  10621  pfxccatin12lem3  14703  prodeq2w  15882  prodeq2ii  15883  prodeq2sdv  15895  divalg  16379  dfgcd2  16522  iscatd2  17648  posi  18284  issubg3  19082  pmtrfrn  19394  psgnunilem2  19431  psgnunilem3  19432  lmhmpropd  20986  lbsacsbs  21072  frlmphl  21696  neiptoptop  23024  neiptopnei  23025  cnhaus  23247  nrmsep  23250  dishaus  23275  ordthauslem  23276  nconnsubb  23316  pthaus  23531  txhaus  23540  xkohaus  23546  regr1lem  23632  isust  24097  ustuqtop4  24138  methaus  24414  metnrmlem3  24756  iscau4  25185  pmltpclem1  25355  dvfsumlem2  25939  dvfsumlem2OLD  25940  aannenlem1  26242  aannenlem2  26243  brsslt  27703  istrkgcb  28389  hlbtwn  28544  iscgra  28742  dfcgra2  28763  f1otrge  28805  axlowdim  28894  axeuclidlem  28895  eengtrkg  28919  clwwlk  29918  upgr3v3e3cycl  30115  upgr4cycl4dv4e  30120  numclwwlk5  30323  ex-opab  30367  l2p  30414  vciOLD  30496  isvclem  30512  isnvlem  30545  dipass  30780  adj1  31868  adjeq  31870  cnlnssadj  32015  br8d  32544  dvdsruasso2  33363  dfufd2lem  33526  constrsuc  33734  constrconj  33741  constrllcllem  33748  constrcbvlem  33751  carsgmon  34311  carsgsigalem  34312  carsgclctunlem2  34316  carsgclctun  34318  bnj1154  34995  br8  35738  br6  35739  br4  35740  fvtransport  36015  brcgr3  36029  brfs  36062  fscgr  36063  btwnconn1lem11  36080  brsegle  36091  fvray  36124  linedegen  36126  fvline  36127  cbvproddavw  36263  bj-isclm  37274  poimirlem28  37637  poimirlem32  37641  heiborlem2  37801  hlsuprexch  39370  3dim1lem5  39455  lplni2  39526  2llnjN  39556  lvoli2  39570  2lplnj  39609  cdleme18d  40284  cdlemg1cex  40577  ismrc  42682  monotoddzzfi  42924  oddcomabszz  42926  zindbi  42928  rmydioph  42996  nnoeomeqom  43294  rp-brsslt  43405  fsumiunss  45566  sumnnodd  45621  stoweidlem31  46022  stoweidlem34  46025  stoweidlem43  46034  stoweidlem48  46039  fourierdlem42  46140  sge0iunmptlemre  46406  sge0iunmpt  46409  vonioo  46673  vonicc  46676  fundcmpsurinjpreimafv  47399  upgrimpths  47899  cycl3grtri  47936  grimgrtri  47938  usgrgrtrirex  47939  grlimgrtri  47985  sepfsepc  48906  iscnrm3rlem8  48925  iscnrm3llem2  48928