Theorem 3anbi123d 1433

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  3anbi12d  1434  3anbi13d  1435  3anbi23d  1436  ax12wdemo  2136  limeq  6186  f13dfv  7029  epne3  7500  oteqimp  7718  wfrlem1  7970  wfrlem15  7985  smoeq  8003  ereq1  8312  indexfi  8878  hartogslem1  9052  tz9.1  9217  updjud  9409  alephval3  9583  cofsmo  9742  cfsmolem  9743  alephsing  9749  axdc3lem2  9924  axdc3lem3  9925  axdc3  9927  axdc4lem  9928  zornn0g  9978  fpwwe2lem4  10107  canthwelem  10123  canthwe  10124  pwfseqlem4a  10134  pwfseqlem4  10135  elwina  10159  elina  10160  iswun  10177  elgrug  10265  iccshftr  12931  iccshftl  12933  iccdil  12935  icccntr  12937  fzaddel  13003  elfzomelpfzo  13203  axdc4uzlem  13413  wrdl1s1  14028  wwlktovf  14380  wwlktovf1  14381  wwlktovfo  14382  wrd2f1tovbij  14384  dfrtrcl2  14482  sqrmo  14672  resqrtcl  14674  resqrtthlem  14675  sqrtneg  14688  sqreu  14781  sqrtthlem  14783  eqsqrtd  14788  prodeq1f  15323  zprod  15352  divalglem10  15816  dfgcd2  15959  coprmprod  16071  pythagtriplem18  16238  pythagtriplem19  16239  prmgaplem3  16458  prmgaplem4  16459  isstruct2  16565  imasval  16856  mreexexlemd  16987  catidd  17023  iscatd2  17024  subsubc  17196  isfunc  17207  funcres2b  17240  ispos  17637  posi  17640  isposd  17645  pospropd  17824  isps  17892  imasmnd2  18028  sgrp2rid2ex  18172  imasgrp2  18295  psgnunilem3  18705  isringd  19420  imasring  19454  isdrngd  19609  islmod  19720  lmodlema  19721  islmodd  19722  lmodprop2d  19778  lmhmpropd  19927  isphl  20407  isphld  20433  phlpropd  20434  assapropd  20648  mdetunilem3  21328  mdetunilem9  21334  fiinopn  21615  iscldtop  21809  lmfval  21946  connsuba  22134  1stcfb  22159  2ndcctbss  22169  subislly  22195  ptval  22284  elpt  22286  elptr  22287  upxp  22337  isfbas  22543  ustval  22917  isust  22918  ustincl  22922  ustdiag  22923  ustinvel  22924  ustexhalf  22925  ust0  22934  imasdsf1olem  23089  tngngp3  23372  lmhmclm  23802  iscph  23885  iscau2  23991  pmltpclem1  24162  isi1f  24388  mbfi1fseqlem6  24434  iblcnlem  24502  dvfsumlem4  24742  aannenlem1  25037  aannenlem2  25038  ulmval  25088  istrkgb  26362  istrkge  26364  istrkgld  26366  istrkg2ld  26367  istrkg3ld  26368  axtgupdim2  26378  axtgeucl  26379  trgcgrg  26422  ishlg  26509  colline  26556  iscgra  26716  isinag  26745  brbtwn  26806  axpaschlem  26847  axlowdim  26868  axeuclid  26870  eengtrkge  26894  issubgr  27174  nb3grpr  27285  nb3grpr2  27286  cplgr3v  27338  wksfval  27512  iswlk  27513  upgr2wlk  27571  wlkiswwlks2  27774  wwlksnextfun  27797  wwlksnextinj  27798  wwlksnextbij  27801  wwlksnextprop  27811  2wlkdlem4  27827  umgr2wlk  27848  umgrwwlks2on  27856  elwspths2spth  27866  isclwwlk  27882  clwlkclwwlklem1  27897  erclwwlkeq  27916  clwwlkn1loopb  27941  erclwwlkneq  27965  s2elclwwlknon2  28002  3wlkdlem5  28061  3wlkdlem6  28063  3wlkdlem9  28066  3wlkdlem10  28067  uhgr3cyclex  28080  upgr4cycl4dv4e  28083  frgr3v  28173  3cyclfrgrrn1  28183  extwwlkfabel  28251  isplig  28372  lpni  28376  isgrpo  28393  vciOLD  28457  isvclem  28473  isnvlem  28506  sspval  28619  isssp  28620  ajfval  28705  dipdir  28738  siilem2  28748  issh  29104  elunop2  29909  superpos  30250  padct  30591  resspos  30781  isslmd  30994  slmdlema  30995  elrspunidl  31140  locfinreflem  31324  locfinref  31325  zarcmplem  31365  zhmnrg  31449  ismntoplly  31507  issiga  31612  isrnsiga  31613  isldsys  31656  rossros  31680  ismeas  31699  isrnmeas  31700  pmeasmono  31823  pmeasadd  31824  istrkg2d  32178  axtgupdim2ALTV  32180  afsval  32183  brafs  32184  bnj919  32279  bnj976  32290  bnj607  32429  bnj873  32437  cvmlift3lem2  32811  cvmlift3lem6  32815  cvmlift3lem7  32816  cvmlift3lem9  32818  cvmlift3  32819  mclsppslem  33074  dfon2lem1  33288  dfon2lem3  33290  dfon2lem7  33294  xpord2lem  33357  poxp2  33358  xpord3lem  33363  xpord3pred  33366  frrlem1  33398  frrlem13  33410  on2ind  33426  on3ind  33427  nodense  33493  nosupprefixmo  33501  noinfprefixmo  33502  nosupcbv  33503  nosupfv  33507  noinfcbv  33518  noinffv  33522  noetalem2  33543  eqscut  33595  no2indslem  33694  brofs  33891  ofscom  33893  btwnouttr  33910  brifs  33929  cgr3com  33939  brcolinear  33945  brfs  33965  unblimceq0lem  34270  knoppndvlem21  34296  csbwrecsg  35059  rdgeqoa  35102  poimirlem4  35376  poimirlem27  35399  mblfinlem3  35411  indexa  35486  sdclem1  35496  fdc  35498  neificl  35506  heiborlem2  35565  isass  35599  ismndo2  35627  isrngo  35650  rngomndo  35688  isgrpda  35708  igenval2  35819  eleqvrels2  36302  eleqvrels3  36303  eqvreleq  36312  lshpset2N  36730  isopos  36791  oposlem  36793  cmtfvalN  36821  cvrfval  36879  3dimlem1  37069  3dim1lem5  37077  lplni2  37148  lvoli2  37192  4atlem11  37220  dalawlem15  37496  cdlemftr3  38176  tendofset  38369  tendoset  38370  istendo  38371  cdlemk28-3  38519  cdlemkid3N  38544  cdlemkid4  38545  lpolsetN  39093  islpolN  39094  lpolconN  39098  ismrc  40060  rabren3dioph  40174  irrapxlem5  40185  rmydioph  40373  mpaaeu  40512  mpaaval  40513  mpaalem  40514  dfsucon  40649  dfrtrcl3  40852  brco3f1o  41154  grumnud  41412  eliooshift  42554  stoweidlem5  43058  stoweidlem18  43071  stoweidlem28  43081  stoweidlem31  43084  stoweidlem41  43094  stoweidlem43  43096  stoweidlem44  43097  stoweidlem45  43098  stoweidlem51  43104  stoweidlem55  43108  stoweidlem59  43112  issal  43367  fundcmpsurbijinjpreimafv  44351  fundcmpsurbijinj  44354  fundcmpsurinjALT  44356  ichnreuop  44416  proththdlem  44557  6gbe  44715  8gbe  44717  bgoldbtbndlem2  44750  bgoldbtbndlem3  44751  bgoldbtbnd  44753  upwlksfval  44789  isupwlk  44790  el0ldep  45299  ldepspr  45306  lmod1  45325  zlmodzxzldep  45337