Theorem 3anbi123d 1438

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ 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:  3anbi12d  1439  3anbi13d  1440  3anbi23d  1441  ax12wdemo  2136  limeq  6344  f13dfv  7249  epne3  7749  oteqimp  7987  xpord2lem  8121  poxp2  8122  xpord3lem  8128  xpord3pred  8131  csbfrecsg  8263  frrlem1  8265  frrlem13  8277  smoeq  8319  on2ind  8633  on3ind  8634  naddasslem1  8658  naddasslem2  8659  naddass  8660  ereq1  8678  sbthfi  9163  indexfi  9311  hartogslem1  9495  brttrcl2  9667  ssttrcl  9668  ttrcltr  9669  ttrclss  9673  ttrclselem2  9679  tz9.1  9682  updjud  9887  alephval3  10063  cofsmo  10222  cfsmolem  10223  alephsing  10229  axdc3lem2  10404  axdc3lem3  10405  axdc3  10407  axdc4lem  10408  zornn0g  10458  fpwwe2lem4  10587  canthwelem  10603  canthwe  10604  pwfseqlem4a  10614  pwfseqlem4  10615  elwina  10639  elina  10640  iswun  10657  elgrug  10745  iccshftr  13447  iccshftl  13449  iccdil  13451  icccntr  13453  fzaddel  13519  elfzomelpfzo  13732  axdc4uzlem  13948  hash3tpb  14460  wrdl1s1  14579  wwlktovf  14922  wwlktovf1  14923  wwlktovfo  14924  wrd2f1tovbij  14926  dfrtrcl2  15028  sqrmo  15217  resqrtcl  15219  resqrtthlem  15220  sqrtneg  15233  sqreu  15327  sqrtthlem  15329  eqsqrtd  15334  prodeq1f  15872  prodeq1  15873  zprod  15903  divalglem10  16372  dfgcd2  16516  coprmprod  16631  pythagtriplem18  16803  pythagtriplem19  16804  prmgaplem3  17024  prmgaplem4  17025  isstruct2  17119  imasval  17474  mreexexlemd  17605  catidd  17641  iscatd2  17642  subsubc  17815  isfunc  17826  funcres2b  17859  ispos  18275  posi  18278  isposd  18283  pospropd  18286  isps  18527  imasmnd2  18701  sgrp2rid2ex  18854  imasgrp2  18987  psgnunilem3  19426  isrngd  20082  imasrng  20086  isringd  20200  imasring  20239  subrngpropd  20477  isdrngd  20674  isdrngdOLD  20676  islmod  20770  lmodlema  20771  islmodd  20772  lmodprop2d  20830  lmhmpropd  20980  isphl  21537  isphld  21563  phlpropd  21564  mdetunilem3  22501  mdetunilem9  22507  fiinopn  22788  iscldtop  22982  lmfval  23119  connsuba  23307  1stcfb  23332  2ndcctbss  23342  subislly  23368  ptval  23457  elpt  23459  elptr  23460  upxp  23510  isfbas  23716  ustval  24090  isust  24091  ustincl  24095  ustdiag  24096  ustinvel  24097  ustexhalf  24098  ust0  24107  imasdsf1olem  24261  tngngp3  24544  lmhmclm  24987  iscph  25070  iscau2  25177  pmltpclem1  25349  isi1f  25575  mbfi1fseqlem6  25621  iblcnlem  25690  dvfsumlem4  25936  aannenlem1  26236  aannenlem2  26237  ulmval  26289  nodense  27604  nosupprefixmo  27612  noinfprefixmo  27613  nosupcbv  27614  nosupfv  27618  noinfcbv  27629  noinffv  27633  noetalem2  27654  eqscut  27717  no2indslem  27861  no3inds  27865  addsproplem3  27878  negsproplem3  27936  mulsproplem10  28028  istrkgb  28382  istrkge  28384  istrkgld  28386  istrkg2ld  28387  istrkg3ld  28388  axtgupdim2  28398  axtgeucl  28399  trgcgrg  28442  ishlg  28529  colline  28576  iscgra  28736  isinag  28765  brbtwn  28826  axpaschlem  28867  axlowdim  28888  axeuclid  28890  eengtrkge  28914  issubgr  29198  nb3grpr  29309  nb3grpr2  29310  cplgr3v  29362  wksfval  29537  iswlk  29538  upgr2wlk  29596  wlkiswwlks2  29805  wwlksnextfun  29828  wwlksnextinj  29829  wwlksnextbij  29832  wwlksnextprop  29842  2wlkdlem4  29858  umgr2wlk  29879  umgrwwlks2on  29887  elwspths2spth  29897  isclwwlk  29913  clwlkclwwlklem1  29928  erclwwlkeq  29947  clwwlkn1loopb  29972  erclwwlkneq  29996  s2elclwwlknon2  30033  3wlkdlem5  30092  3wlkdlem6  30094  3wlkdlem9  30097  3wlkdlem10  30098  uhgr3cyclex  30111  upgr4cycl4dv4e  30114  frgr3v  30204  3cyclfrgrrn1  30214  extwwlkfabel  30282  isplig  30405  lpni  30409  isgrpo  30426  vciOLD  30490  isvclem  30506  isnvlem  30539  sspval  30652  isssp  30653  ajfval  30738  dipdir  30771  siilem2  30781  issh  31137  elunop2  31942  superpos  32283  padct  32643  resspos  32892  isslmd  33155  slmdlema  33156  subsdrg  33248  elrspunidl  33399  constrcbvlem  33745  locfinreflem  33830  locfinref  33831  zarcmplem  33871  zhmnrg  33955  ismntoplly  34015  issiga  34102  isrnsiga  34103  isldsys  34146  rossros  34170  ismeas  34189  isrnmeas  34190  pmeasmono  34315  pmeasadd  34316  istrkg2d  34657  axtgupdim2ALTV  34659  afsval  34662  brafs  34663  bnj919  34757  bnj976  34767  bnj607  34906  bnj873  34914  cvmlift3lem2  35307  cvmlift3lem6  35311  cvmlift3lem7  35312  cvmlift3lem9  35314  cvmlift3  35315  mclsppslem  35570  dfon2lem1  35771  dfon2lem3  35773  dfon2lem7  35777  brofs  35993  ofscom  35995  btwnouttr  36012  brifs  36031  cgr3com  36041  brcolinear  36047  brfs  36067  prodeq12sdv  36206  cbvproddavw2  36284  unblimceq0lem  36494  knoppndvlem21  36520  rdgeqoa  37358  poimirlem4  37618  poimirlem27  37641  mblfinlem3  37653  indexa  37727  sdclem1  37737  fdc  37739  neificl  37747  heiborlem2  37806  isass  37840  ismndo2  37868  isrngo  37891  rngomndo  37929  isgrpda  37949  igenval2  38060  eleqvrels2  38583  eleqvrels3  38584  eqvreleq  38593  lshpset2N  39112  isopos  39173  oposlem  39175  cmtfvalN  39203  cvrfval  39261  3dimlem1  39452  3dim1lem5  39460  lplni2  39531  lvoli2  39575  4atlem11  39603  dalawlem15  39879  cdlemftr3  40559  tendofset  40752  tendoset  40753  istendo  40754  cdlemk28-3  40902  cdlemkid3N  40927  cdlemkid4  40928  lpolsetN  41476  islpolN  41477  lpolconN  41481  isprimroot  42081  aks6d1c1p1  42095  ismrc  42689  rabren3dioph  42803  irrapxlem5  42814  rmydioph  43003  mpaaeu  43139  mpaaval  43140  mpaalem  43141  naddwordnexlem4  43390  dfsucon  43512  minregex  43523  dfrtrcl3  43722  brco3f1o  44022  grumnud  44275  modelaxreplem1  44968  modelaxreplem2  44969  modelaxrep  44971  eliooshift  45504  stoweidlem5  46003  stoweidlem18  46016  stoweidlem28  46026  stoweidlem31  46029  stoweidlem41  46039  stoweidlem43  46041  stoweidlem44  46042  stoweidlem45  46043  stoweidlem51  46049  stoweidlem55  46053  stoweidlem59  46057  issal  46312  fundcmpsurbijinjpreimafv  47408  fundcmpsurbijinj  47411  fundcmpsurinjALT  47413  ichnreuop  47473  proththdlem  47614  6gbe  47772  8gbe  47774  bgoldbtbndlem2  47807  bgoldbtbndlem3  47808  bgoldbtbnd  47810  grtriproplem  47938  grtri  47939  grtrif1o  47941  isgrtri  47942  grimgrtri  47948  usgrexmpl1tri  48016  gpgvtx0  48044  gpgvtx1  48045  gpgedgvtx0  48052  gpgedgvtx1  48053  upwlksfval  48123  isupwlk  48124  el0ldep  48455  ldepspr  48462  lmod1  48481  zlmodzxzldep  48493  catprs  49000  catprsc  49002  prsthinc  49453  2arwcatlem1  49584  cnelsubclem  49592