Theorem 3anbi123d 1437

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  3anbi12d  1438  3anbi13d  1439  3anbi23d  1440  ax12wdemo  2132  limeq  6373  f13dfv  7267  epne3  7755  oteqimp  7989  xpord2lem  8123  poxp2  8124  xpord3lem  8130  xpord3pred  8133  csbfrecsg  8264  frrlem1  8266  frrlem13  8278  wfrlem1OLD  8303  wfrlem15OLD  8318  smoeq  8345  on2ind  8664  on3ind  8665  naddasslem1  8689  naddasslem2  8690  naddass  8691  ereq1  8706  sbthfi  9198  indexfi  9356  hartogslem1  9533  brttrcl2  9705  ssttrcl  9706  ttrcltr  9707  ttrclss  9711  ttrclselem2  9717  tz9.1  9720  updjud  9925  alephval3  10101  cofsmo  10260  cfsmolem  10261  alephsing  10267  axdc3lem2  10442  axdc3lem3  10443  axdc3  10445  axdc4lem  10446  zornn0g  10496  fpwwe2lem4  10625  canthwelem  10641  canthwe  10642  pwfseqlem4a  10652  pwfseqlem4  10653  elwina  10677  elina  10678  iswun  10695  elgrug  10783  iccshftr  13459  iccshftl  13461  iccdil  13463  icccntr  13465  fzaddel  13531  elfzomelpfzo  13732  axdc4uzlem  13944  wrdl1s1  14560  wwlktovf  14903  wwlktovf1  14904  wwlktovfo  14905  wrd2f1tovbij  14907  dfrtrcl2  15005  sqrmo  15194  resqrtcl  15196  resqrtthlem  15197  sqrtneg  15210  sqreu  15303  sqrtthlem  15305  eqsqrtd  15310  prodeq1f  15848  zprod  15877  divalglem10  16341  dfgcd2  16484  coprmprod  16594  pythagtriplem18  16761  pythagtriplem19  16762  prmgaplem3  16982  prmgaplem4  16983  isstruct2  17078  imasval  17453  mreexexlemd  17584  catidd  17620  iscatd2  17621  subsubc  17799  isfunc  17810  funcres2b  17843  ispos  18263  posi  18266  isposd  18272  pospropd  18276  isps  18517  imasmnd2  18658  sgrp2rid2ex  18804  imasgrp2  18934  psgnunilem3  19357  isringd  20095  imasring  20133  isdrngd  20336  isdrngdOLD  20338  islmod  20463  lmodlema  20464  islmodd  20465  lmodprop2d  20522  lmhmpropd  20672  isphl  21165  isphld  21191  phlpropd  21192  mdetunilem3  22098  mdetunilem9  22104  fiinopn  22385  iscldtop  22581  lmfval  22718  connsuba  22906  1stcfb  22931  2ndcctbss  22941  subislly  22967  ptval  23056  elpt  23058  elptr  23059  upxp  23109  isfbas  23315  ustval  23689  isust  23690  ustincl  23694  ustdiag  23695  ustinvel  23696  ustexhalf  23697  ust0  23706  imasdsf1olem  23861  tngngp3  24155  lmhmclm  24585  iscph  24669  iscau2  24776  pmltpclem1  24947  isi1f  25173  mbfi1fseqlem6  25220  iblcnlem  25288  dvfsumlem4  25528  aannenlem1  25823  aannenlem2  25824  ulmval  25874  nodense  27175  nosupprefixmo  27183  noinfprefixmo  27184  nosupcbv  27185  nosupfv  27189  noinfcbv  27200  noinffv  27204  noetalem2  27225  eqscut  27286  no2indslem  27418  no3inds  27422  addsproplem3  27435  negsproplem3  27484  mulsproplem10  27561  istrkgb  27686  istrkge  27688  istrkgld  27690  istrkg2ld  27691  istrkg3ld  27692  axtgupdim2  27702  axtgeucl  27703  trgcgrg  27746  ishlg  27833  colline  27880  iscgra  28040  isinag  28069  brbtwn  28137  axpaschlem  28178  axlowdim  28199  axeuclid  28201  eengtrkge  28225  issubgr  28508  nb3grpr  28619  nb3grpr2  28620  cplgr3v  28672  wksfval  28846  iswlk  28847  upgr2wlk  28905  wlkiswwlks2  29109  wwlksnextfun  29132  wwlksnextinj  29133  wwlksnextbij  29136  wwlksnextprop  29146  2wlkdlem4  29162  umgr2wlk  29183  umgrwwlks2on  29191  elwspths2spth  29201  isclwwlk  29217  clwlkclwwlklem1  29232  erclwwlkeq  29251  clwwlkn1loopb  29276  erclwwlkneq  29300  s2elclwwlknon2  29337  3wlkdlem5  29396  3wlkdlem6  29398  3wlkdlem9  29401  3wlkdlem10  29402  uhgr3cyclex  29415  upgr4cycl4dv4e  29418  frgr3v  29508  3cyclfrgrrn1  29518  extwwlkfabel  29586  isplig  29707  lpni  29711  isgrpo  29728  vciOLD  29792  isvclem  29808  isnvlem  29841  sspval  29954  isssp  29955  ajfval  30040  dipdir  30073  siilem2  30083  issh  30439  elunop2  31244  superpos  31585  padct  31922  resspos  32114  isslmd  32325  slmdlema  32326  elrspunidl  32504  locfinreflem  32758  locfinref  32759  zarcmplem  32799  zhmnrg  32885  ismntoplly  32943  issiga  33048  isrnsiga  33049  isldsys  33092  rossros  33116  ismeas  33135  isrnmeas  33136  pmeasmono  33261  pmeasadd  33262  istrkg2d  33616  axtgupdim2ALTV  33618  afsval  33621  brafs  33622  bnj919  33716  bnj976  33726  bnj607  33865  bnj873  33873  cvmlift3lem2  34249  cvmlift3lem6  34253  cvmlift3lem7  34254  cvmlift3lem9  34256  cvmlift3  34257  mclsppslem  34512  dfon2lem1  34693  dfon2lem3  34695  dfon2lem7  34699  brofs  34915  ofscom  34917  btwnouttr  34934  brifs  34953  cgr3com  34963  brcolinear  34969  brfs  34989  unblimceq0lem  35320  knoppndvlem21  35346  rdgeqoa  36189  poimirlem4  36430  poimirlem27  36453  mblfinlem3  36465  indexa  36539  sdclem1  36549  fdc  36551  neificl  36559  heiborlem2  36618  isass  36652  ismndo2  36680  isrngo  36703  rngomndo  36741  isgrpda  36761  igenval2  36872  eleqvrels2  37400  eleqvrels3  37401  eqvreleq  37410  lshpset2N  37927  isopos  37988  oposlem  37990  cmtfvalN  38018  cvrfval  38076  3dimlem1  38267  3dim1lem5  38275  lplni2  38346  lvoli2  38390  4atlem11  38418  dalawlem15  38694  cdlemftr3  39374  tendofset  39567  tendoset  39568  istendo  39569  cdlemk28-3  39717  cdlemkid3N  39742  cdlemkid4  39743  lpolsetN  40291  islpolN  40292  lpolconN  40296  ismrc  41372  rabren3dioph  41486  irrapxlem5  41497  rmydioph  41686  mpaaeu  41825  mpaaval  41826  mpaalem  41827  naddwordnexlem4  42085  dfsucon  42207  minregex  42218  dfrtrcl3  42417  brco3f1o  42717  grumnud  42978  eliooshift  44154  stoweidlem5  44656  stoweidlem18  44669  stoweidlem28  44679  stoweidlem31  44682  stoweidlem41  44692  stoweidlem43  44694  stoweidlem44  44695  stoweidlem45  44696  stoweidlem51  44702  stoweidlem55  44706  stoweidlem59  44710  issal  44965  fundcmpsurbijinjpreimafv  46010  fundcmpsurbijinj  46013  fundcmpsurinjALT  46015  ichnreuop  46075  proththdlem  46216  6gbe  46374  8gbe  46376  bgoldbtbndlem2  46409  bgoldbtbndlem3  46410  bgoldbtbnd  46412  upwlksfval  46448  isupwlk  46449  isrngd  46607  imasrng  46613  subrngpropd  46680  el0ldep  47049  ldepspr  47056  lmod1  47075  zlmodzxzldep  47087  catprs  47533  catprsc  47535  prsthinc  47576