Theorem 3anbi123d 1464

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3anbi12d  1465  3anbi13d  1466  3anbi23d  1467  ax12wdemo  2172  limeq  6373  f13dfv  7280  epne3  7785  oteqimp  8018  xpord2lem  8152  poxp2  8153  xpord3lem  8159  xpord3pred  8162  csbfrecsg  8295  frrlem1  8297  frrlem13  8309  smoeq  8351  on2ind  8671  on3ind  8672  naddasslem1  8697  naddasslem2  8698  naddass  8699  ereq1  8718  sbthfi  9207  indexfi  9342  hartogslem1  9529  brttrcl2  9708  ssttrcl  9709  ttrcltr  9710  ttrclss  9714  ttrclselem2  9720  tz9.1  9723  updjud  10008  alephval3  10182  cofsmo  10340  cfsmolem  10341  alephsing  10347  axdc3lem2  10522  axdc3lem3  10523  axdc3  10525  axdc4lem  10526  zornn0g  10576  fpwwe2lem4  10712  canthwelem  10728  canthwe  10729  pwfseqlem4a  10739  pwfseqlem4  10740  elwina  10764  elina  10765  iswun  10782  elgrug  10870  iccshftr  13610  iccshftl  13612  iccdil  13614  icccntr  13616  fzaddel  13685  elfzomelpfzo  13900  axdc4uzlem  14119  hash3tpb  14633  wrdl1s1  14755  wwlktovf  15102  wwlktovf1  15103  wwlktovfo  15104  wrd2f1tovbij  15106  dfrtrcl2  15208  sqrmo  15411  resqrtcl  15413  resqrtthlem  15414  sqrtneg  15427  sqreu  15521  sqrtthlem  15523  eqsqrtd  15528  prodeq1f  16068  prodeq1  16069  zprod  16097  divalglem10  16565  dfgcd2  16712  coprmprod  16829  pythagtriplem18  17003  pythagtriplem19  17004  prmgaplem3  17224  prmgaplem4  17225  isstruct2  17320  imasval  17676  mreexexlemd  17811  catidd  17847  iscatd2  17848  subsubc  18021  isfunc  18032  funcres2b  18065  ispos  18481  posi  18484  isposd  18489  pospropd  18492  resspos  18596  isps  18735  imasmnd2  18961  sgrp2rid2ex  19119  imasgrp2  19258  psgnunilem3  19703  isrngd  20388  imasrng  20392  isringd  20515  imasring  20553  subrngpropd  20813  isdrngd  21015  isdrngdOLD  21017  islmod  21132  lmodlema  21133  islmodd  21134  lmodprop2d  21192  lmhmpropd  21341  rspprop  21517  isphl  21927  isphld  21953  phlpropd  21954  mdetunilem3  22922  mdetunilem9  22928  fiinopn  23212  iscldtop  23406  lmfval  23543  connsuba  23731  1stcfb  23756  2ndcctbss  23767  subislly  23793  ptval  23882  elpt  23884  elptr  23885  upxp  23935  isfbas  24141  ustval  24515  isust  24516  ustincl  24520  ustdiag  24521  ustinvel  24522  ustexhalf  24523  ust0  24532  imasdsf1olem  24685  tngngp3  24968  lmhmclm  25401  iscph  25484  iscau2  25591  pmltpclem1  25762  isi1f  25988  mbfi1fseqlem6  26034  iblcnlem  26102  dvfsumlem4  26342  aannenlem1  26648  aannenlem2  26649  ulmval  26700  nodense  28042  nosupprefixmo  28050  noinfprefixmo  28051  nosupcbv  28052  nosupfv  28056  noinfcbv  28067  noinffv  28071  noetalem2  28092  eqcuts  28164  no2indlesm  28333  no3inds  28337  addsproplem3  28350  negsproplem3  28409  mulsproplem10  28504  bdayfinbndcbv  28845  bdayfinbndlem1  28846  bdayfinbndlem2  28847  istrkgb  28910  istrkge  28912  istrkgld  28914  istrkg2ld  28915  istrkg3ld  28916  axtgupdim2  28926  axtgeucl  28927  trgcgrg  28971  ishlg2  29058  ishlg  29061  colline  29111  iscgra  29309  isinag  29350  cgrabasimass  29371  angmgmaddov1  29381  angmgmaddcl  29384  angmgmval  29387  brbtwn  29470  axpaschlem  29511  axlowdim  29532  axeuclid  29534  eengtrkge  29558  issubgr  29845  nb3grpr  29956  nb3grpr2  29957  cplgr3v  30009  wksfval  30183  iswlk  30184  upgr2wlk  30240  wlkiswwlks2  30457  wwlksnextfun  30480  wwlksnextinj  30481  wwlksnextbij  30484  wwlksnextprop  30494  2wlkdlem4  30510  umgr2wlk  30531  usgrwwlks2on  30540  umgrwwlks2on  30541  elwspths2spth  30552  isclwwlk  30568  clwlkclwwlklem1  30583  erclwwlkeq  30602  clwwlkn1loopb  30627  erclwwlkneq  30651  s2elclwwlknon2  30688  3wlkdlem5  30757  3wlkdlem6  30759  3wlkdlem9  30762  3wlkdlem10  30763  uhgr3cyclex  30776  upgr4cycl4dv4e  30779  frgr3v  30869  3cyclfrgrrn1  30879  extwwlkfabel  30947  isplig  31071  lpni  31075  isgrpo  31092  vciOLD  31156  isvclem  31172  isnvlem  31205  sspval  31318  isssp  31319  ajfval  31404  dipdir  31437  siilem2  31447  issh  31803  elunop2  32608  superpos  32949  padct  33303  isslmd  33756  slmdlema  33757  subsdrg  33853  elrspunidl  33971  constrcbvlem  34380  locfinreflem  34465  locfinref  34466  zarcmplem  34506  zhmnrg  34590  ismntoplly  34650  issiga  34737  isrnsiga  34738  isldsys  34782  rossros  34806  ismeas  34825  isrnmeas  34826  pmeasmono  34949  pmeasadd  34950  istrkg2d  35288  axtgupdim2ALTV  35290  afsval  35296  brafs  35297  bnj919  35391  bnj976  35401  bnj607  35539  bnj873  35547  fineqvnttrclse  35775  tz9.1regs  35785  cvmlift3lem2  36064  cvmlift3lem6  36068  cvmlift3lem7  36069  cvmlift3lem9  36071  cvmlift3  36072  mclsppslem  36327  dfon2lem1  36525  dfon2lem3  36527  dfon2lem7  36531  brofs  36750  ofscom  36752  btwnouttr  36769  brifs  36788  cgr3com  36798  brcolinear  36804  brfs  36824  prodeq12sdv  36987  cbvproddavw2  37065  unblimceq0lem  37352  knoppndvlem21  37378  rdgeqoa  38273  poimirlem4  38522  poimirlem27  38545  mblfinlem3  38557  indexa  38647  sdclem1  38657  fdc  38659  neificl  38667  heiborlem2  38726  isass  38760  ismndo2  38788  isrngo  38811  rngomndo  38849  isgrpda  38869  igenval2  38980  eleqvrels2  39588  eleqvrels3  39589  eqvreleq  39598  lshpset2N  40156  isopos  40217  oposlem  40219  cmtfvalN  40247  cvrfval  40305  3dimlem1  40495  3dim1lem5  40503  lplni2  40574  lvoli2  40618  4atlem11  40646  dalawlem15  40922  cdlemftr3  41602  tendofset  41795  tendoset  41796  istendo  41797  cdlemk28-3  41945  cdlemkid3N  41970  cdlemkid4  41971  lpolsetN  42519  islpolN  42520  lpolconN  42524  isprimroot  43123  aks6d1c1p1  43137  ismrc  43691  rabren3dioph  43801  irrapxlem5  43812  rmydioph  44000  mpaaeu  44136  mpaaval  44137  mpaalem  44138  naddwordnexlem4  44387  dfsucon  44508  minregex  44519  dfrtrcl3  44718  brco3f1o  45018  grumnud  45255  modelaxreplem1  45946  modelaxreplem2  45947  modelaxrep  45949  eliooshift  46487  stoweidlem5  46984  stoweidlem18  46997  stoweidlem28  47007  stoweidlem31  47010  stoweidlem41  47020  stoweidlem43  47022  stoweidlem44  47023  stoweidlem45  47024  stoweidlem51  47030  stoweidlem55  47034  stoweidlem59  47038  issal  47293  fundcmpsurbijinjpreimafv  48458  fundcmpsurbijinj  48461  fundcmpsurinjALT  48463  ichnreuop  48523  proththdlem  48667  6gbe  48838  8gbe  48840  bgoldbtbndlem2  48873  bgoldbtbndlem3  48874  bgoldbtbnd  48876  grtriproplem  49006  grtri  49007  grtrif1o  49009  isgrtri  49010  grimgrtri  49016  usgrexmpl1tri  49092  gpgvtx0  49120  gpgvtx1  49121  gpgedgvtx0  49128  gpgedgvtx1  49129  upwlksfval  49202  isupwlk  49203  el0ldep  49547  ldepspr  49554  lmod1  49573  zlmodzxzldep  49585  catprs  50088  catprsc  50090  prsthinc  50541  2arwcatlem1  50672  cnelsubclem  50680