Theorem 3anbi123d 1432

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  3anbi12d  1433  3anbi13d  1434  3anbi23d  1435  ax12wdemo  2139  limeq  6203  f13dfv  7031  epne3  7495  oteqimp  7708  wfrlem1  7954  wfrlem15  7969  smoeq  7987  ereq1  8296  indexfi  8832  hartogslem1  9006  tz9.1  9171  updjud  9363  alephval3  9536  cofsmo  9691  cfsmolem  9692  alephsing  9698  axdc3lem2  9873  axdc3lem3  9874  axdc3  9876  axdc4lem  9877  zornn0g  9927  fpwwe2lem5  10056  canthwelem  10072  canthwe  10073  pwfseqlem4a  10083  pwfseqlem4  10084  elwina  10108  elina  10109  iswun  10126  elgrug  10214  iccshftr  12873  iccshftl  12875  iccdil  12877  icccntr  12879  fzaddel  12942  elfzomelpfzo  13142  axdc4uzlem  13352  wrdl1s1  13968  wwlktovf  14320  wwlktovf1  14321  wwlktovfo  14322  wrd2f1tovbij  14324  dfrtrcl2  14421  sqrmo  14611  resqrtcl  14613  resqrtthlem  14614  sqrtneg  14627  sqreu  14720  sqrtthlem  14722  eqsqrtd  14727  prodeq1f  15262  zprod  15291  divalglem10  15753  dfgcd2  15894  coprmprod  16005  pythagtriplem18  16169  pythagtriplem19  16170  prmgaplem3  16389  prmgaplem4  16390  isstruct2  16493  imasval  16784  mreexexlemd  16915  catidd  16951  iscatd2  16952  subsubc  17123  isfunc  17134  funcres2b  17167  ispos  17557  posi  17560  isposd  17565  pospropd  17744  isps  17812  imasmnd2  17948  sgrp2rid2ex  18092  imasgrp2  18214  psgnunilem3  18624  isringd  19335  imasring  19369  isdrngd  19527  islmod  19638  lmodlema  19639  islmodd  19640  lmodprop2d  19696  lmhmpropd  19845  assapropd  20101  isphl  20772  isphld  20798  phlpropd  20799  mdetunilem3  21223  mdetunilem9  21229  fiinopn  21509  iscldtop  21703  lmfval  21840  connsuba  22028  1stcfb  22053  2ndcctbss  22063  subislly  22089  ptval  22178  elpt  22180  elptr  22181  upxp  22231  isfbas  22437  ustval  22811  isust  22812  ustincl  22816  ustdiag  22817  ustinvel  22818  ustexhalf  22819  ust0  22828  imasdsf1olem  22983  tngngp3  23265  lmhmclm  23691  iscph  23774  iscau2  23880  pmltpclem1  24049  isi1f  24275  mbfi1fseqlem6  24321  iblcnlem  24389  dvfsumlem4  24626  aannenlem1  24917  aannenlem2  24918  ulmval  24968  istrkgb  26241  istrkge  26243  istrkgld  26245  istrkg2ld  26246  istrkg3ld  26247  axtgupdim2  26257  axtgeucl  26258  trgcgrg  26301  ishlg  26388  colline  26435  iscgra  26595  isinag  26624  brbtwn  26685  axpaschlem  26726  axlowdim  26747  axeuclid  26749  eengtrkge  26773  issubgr  27053  nb3grpr  27164  nb3grpr2  27165  cplgr3v  27217  wksfval  27391  iswlk  27392  upgr2wlk  27450  wlkiswwlks2  27653  wwlksnextfun  27676  wwlksnextinj  27677  wwlksnextbij  27680  wwlksnextprop  27691  2wlkdlem4  27707  umgr2wlk  27728  umgrwwlks2on  27736  elwspths2spth  27746  isclwwlk  27762  clwlkclwwlklem1  27777  erclwwlkeq  27796  clwwlkn1loopb  27821  erclwwlkneq  27846  s2elclwwlknon2  27883  3wlkdlem5  27942  3wlkdlem6  27944  3wlkdlem9  27947  3wlkdlem10  27948  uhgr3cyclex  27961  upgr4cycl4dv4e  27964  frgr3v  28054  3cyclfrgrrn1  28064  extwwlkfabel  28132  isplig  28253  lpni  28257  isgrpo  28274  vciOLD  28338  isvclem  28354  isnvlem  28387  sspval  28500  isssp  28501  ajfval  28586  dipdir  28619  siilem2  28629  issh  28985  elunop2  29790  superpos  30131  padct  30455  resspos  30646  isslmd  30830  slmdlema  30831  locfinreflem  31104  locfinref  31105  zhmnrg  31208  ismntoplly  31266  issiga  31371  isrnsiga  31372  isldsys  31415  rossros  31439  ismeas  31458  isrnmeas  31459  pmeasmono  31582  pmeasadd  31583  istrkg2d  31937  axtgupdim2ALTV  31939  afsval  31942  brafs  31943  bnj919  32038  bnj976  32049  bnj607  32188  bnj873  32196  cvmlift3lem2  32567  cvmlift3lem6  32571  cvmlift3lem7  32572  cvmlift3lem9  32574  cvmlift3  32575  mclsppslem  32830  dfon2lem1  33028  dfon2lem3  33030  dfon2lem7  33034  frrlem1  33123  frrlem13  33135  nodense  33196  noprefixmo  33202  nosupfv  33206  noetalem5  33221  noeta  33222  brofs  33466  ofscom  33468  btwnouttr  33485  brifs  33504  cgr3com  33514  brcolinear  33520  brfs  33540  unblimceq0lem  33845  knoppndvlem21  33871  csbwrecsg  34611  rdgeqoa  34654  poimirlem4  34911  poimirlem27  34934  mblfinlem3  34946  indexa  35023  sdclem1  35033  fdc  35035  neificl  35043  heiborlem2  35105  isass  35139  ismndo2  35167  isrngo  35190  rngomndo  35228  isgrpda  35248  igenval2  35359  eleqvrels2  35842  eleqvrels3  35843  eqvreleq  35852  lshpset2N  36270  isopos  36331  oposlem  36333  cmtfvalN  36361  cvrfval  36419  3dimlem1  36609  3dim1lem5  36617  lplni2  36688  lvoli2  36732  4atlem11  36760  dalawlem15  37036  cdlemftr3  37716  tendofset  37909  tendoset  37910  istendo  37911  cdlemk28-3  38059  cdlemkid3N  38084  cdlemkid4  38085  lpolsetN  38633  islpolN  38634  lpolconN  38638  ismrc  39347  rabren3dioph  39461  irrapxlem5  39472  rmydioph  39660  mpaaeu  39799  mpaaval  39800  mpaalem  39801  dfsucon  39938  dfrtrcl3  40127  brco3f1o  40432  grumnud  40671  eliooshift  41831  stoweidlem5  42339  stoweidlem18  42352  stoweidlem28  42362  stoweidlem31  42365  stoweidlem41  42375  stoweidlem43  42377  stoweidlem44  42378  stoweidlem45  42379  stoweidlem51  42385  stoweidlem55  42389  stoweidlem59  42393  issal  42648  fundcmpsurbijinjpreimafv  43616  fundcmpsurbijinj  43619  fundcmpsurinjALT  43621  ichnreuop  43683  proththdlem  43827  6gbe  43985  8gbe  43987  bgoldbtbndlem2  44020  bgoldbtbndlem3  44021  bgoldbtbnd  44023  upwlksfval  44059  isupwlk  44060  el0ldep  44570  ldepspr  44577  lmod1  44596  zlmodzxzldep  44608