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  2173  limeq  6376  f13dfv  7278  epne3  7774  oteqimp  8007  xpord2lem  8140  poxp2  8141  xpord3lem  8147  xpord3pred  8150  csbfrecsg  8283  frrlem1  8285  frrlem13  8297  smoeq  8339  on2ind  8657  on3ind  8658  naddasslem1  8683  naddasslem2  8684  naddass  8685  ereq1  8704  sbthfi  9186  indexfi  9320  hartogslem1  9507  brttrcl2  9686  ssttrcl  9687  ttrcltr  9688  ttrclss  9692  ttrclselem2  9698  tz9.1  9701  updjud  9932  alephval3  10106  cofsmo  10264  cfsmolem  10265  alephsing  10271  axdc3lem2  10446  axdc3lem3  10447  axdc3  10449  axdc4lem  10450  zornn0g  10500  fpwwe2lem4  10630  canthwelem  10646  canthwe  10647  pwfseqlem4a  10657  pwfseqlem4  10658  elwina  10682  elina  10683  iswun  10700  elgrug  10788  iccshftr  13525  iccshftl  13527  iccdil  13529  icccntr  13531  fzaddel  13599  elfzomelpfzo  13814  axdc4uzlem  14033  hash3tpb  14546  wrdl1s1  14668  wwlktovf  15013  wwlktovf1  15014  wwlktovfo  15015  wrd2f1tovbij  15017  dfrtrcl2  15119  sqrmo  15322  resqrtcl  15324  resqrtthlem  15325  sqrtneg  15338  sqreu  15432  sqrtthlem  15434  eqsqrtd  15439  prodeq1f  15979  prodeq1  15980  zprod  16010  divalglem10  16478  dfgcd2  16622  coprmprod  16737  pythagtriplem18  16910  pythagtriplem19  16911  prmgaplem3  17131  prmgaplem4  17132  isstruct2  17227  imasval  17583  mreexexlemd  17718  catidd  17754  iscatd2  17755  subsubc  17928  isfunc  17939  funcres2b  17972  ispos  18388  posi  18391  isposd  18396  pospropd  18399  resspos  18503  isps  18642  imasmnd2  18856  sgrp2rid2ex  19013  imasgrp2  19145  psgnunilem3  19590  isrngd  20275  imasrng  20279  isringd  20400  imasring  20438  subrngpropd  20697  isdrngd  20898  isdrngdOLD  20900  islmod  21015  lmodlema  21016  islmodd  21017  lmodprop2d  21075  lmhmpropd  21224  rspprop  21400  isphl  21808  isphld  21834  phlpropd  21835  mdetunilem3  22801  mdetunilem9  22807  fiinopn  23088  iscldtop  23282  lmfval  23419  connsuba  23607  1stcfb  23632  2ndcctbss  23643  subislly  23669  ptval  23758  elpt  23760  elptr  23761  upxp  23811  isfbas  24017  ustval  24391  isust  24392  ustincl  24396  ustdiag  24397  ustinvel  24398  ustexhalf  24399  ust0  24408  imasdsf1olem  24561  tngngp3  24844  lmhmclm  25277  iscph  25360  iscau2  25467  pmltpclem1  25638  isi1f  25864  mbfi1fseqlem6  25910  iblcnlem  25979  dvfsumlem4  26219  aannenlem1  26522  aannenlem2  26523  ulmval  26574  nodense  27887  nosupprefixmo  27895  noinfprefixmo  27896  nosupcbv  27897  nosupfv  27901  noinfcbv  27912  noinffv  27916  noetalem2  27937  eqcuts  28009  no2indlesm  28178  no3inds  28182  addsproplem3  28195  negsproplem3  28254  mulsproplem10  28349  bdayfinbndcbv  28690  bdayfinbndlem1  28691  bdayfinbndlem2  28692  istrkgb  28755  istrkge  28757  istrkgld  28759  istrkg2ld  28760  istrkg3ld  28761  axtgupdim2  28771  axtgeucl  28772  trgcgrg  28815  ishlg2  28902  ishlg  28905  colline  28954  iscgra  29151  isinag  29186  brbtwn  29280  axpaschlem  29321  axlowdim  29342  axeuclid  29344  eengtrkge  29368  issubgr  29655  nb3grpr  29766  nb3grpr2  29767  cplgr3v  29819  wksfval  29993  iswlk  29994  upgr2wlk  30050  wlkiswwlks2  30267  wwlksnextfun  30290  wwlksnextinj  30291  wwlksnextbij  30294  wwlksnextprop  30304  2wlkdlem4  30320  umgr2wlk  30341  usgrwwlks2on  30350  umgrwwlks2on  30351  elwspths2spth  30362  isclwwlk  30378  clwlkclwwlklem1  30393  erclwwlkeq  30412  clwwlkn1loopb  30437  erclwwlkneq  30461  s2elclwwlknon2  30498  3wlkdlem5  30561  3wlkdlem6  30563  3wlkdlem9  30566  3wlkdlem10  30567  uhgr3cyclex  30580  upgr4cycl4dv4e  30583  frgr3v  30673  3cyclfrgrrn1  30683  extwwlkfabel  30751  isplig  30875  lpni  30879  isgrpo  30896  vciOLD  30960  isvclem  30976  isnvlem  31009  sspval  31122  isssp  31123  ajfval  31208  dipdir  31241  siilem2  31251  issh  31607  elunop2  32412  superpos  32753  padct  33109  isslmd  33562  slmdlema  33563  subsdrg  33659  elrspunidl  33776  constrcbvlem  34185  locfinreflem  34270  locfinref  34271  zarcmplem  34311  zhmnrg  34395  ismntoplly  34455  issiga  34542  isrnsiga  34543  isldsys  34587  rossros  34611  ismeas  34630  isrnmeas  34631  pmeasmono  34755  pmeasadd  34756  istrkg2d  35094  axtgupdim2ALTV  35096  afsval  35102  brafs  35103  bnj919  35197  bnj976  35207  bnj607  35345  bnj873  35353  fineqvnttrclse  35570  tz9.1regs  35580  cvmlift3lem2  35825  cvmlift3lem6  35829  cvmlift3lem7  35830  cvmlift3lem9  35832  cvmlift3  35833  mclsppslem  36088  dfon2lem1  36286  dfon2lem3  36288  dfon2lem7  36292  brofs  36510  ofscom  36512  btwnouttr  36529  brifs  36548  cgr3com  36558  brcolinear  36564  brfs  36584  prodeq12sdv  36763  cbvproddavw2  36841  unblimceq0lem  37128  knoppndvlem21  37154  rdgeqoa  38049  poimirlem4  38308  poimirlem27  38331  mblfinlem3  38343  indexa  38417  sdclem1  38427  fdc  38429  neificl  38437  heiborlem2  38496  isass  38530  ismndo2  38558  isrngo  38581  rngomndo  38619  isgrpda  38639  igenval2  38750  eleqvrels2  39358  eleqvrels3  39359  eqvreleq  39368  lshpset2N  39926  isopos  39987  oposlem  39989  cmtfvalN  40017  cvrfval  40075  3dimlem1  40265  3dim1lem5  40273  lplni2  40344  lvoli2  40388  4atlem11  40416  dalawlem15  40692  cdlemftr3  41372  tendofset  41565  tendoset  41566  istendo  41567  cdlemk28-3  41715  cdlemkid3N  41740  cdlemkid4  41741  lpolsetN  42289  islpolN  42290  lpolconN  42294  isprimroot  42893  aks6d1c1p1  42907  ismrc  43465  rabren3dioph  43575  irrapxlem5  43586  rmydioph  43774  mpaaeu  43910  mpaaval  43911  mpaalem  43912  naddwordnexlem4  44161  dfsucon  44282  minregex  44293  dfrtrcl3  44492  brco3f1o  44792  grumnud  45029  modelaxreplem1  45720  modelaxreplem2  45721  modelaxrep  45723  eliooshift  46255  stoweidlem5  46752  stoweidlem18  46765  stoweidlem28  46775  stoweidlem31  46778  stoweidlem41  46788  stoweidlem43  46790  stoweidlem44  46791  stoweidlem45  46792  stoweidlem51  46798  stoweidlem55  46802  stoweidlem59  46806  issal  47061  fundcmpsurbijinjpreimafv  48189  fundcmpsurbijinj  48192  fundcmpsurinjALT  48194  ichnreuop  48254  proththdlem  48398  6gbe  48569  8gbe  48571  bgoldbtbndlem2  48604  bgoldbtbndlem3  48605  bgoldbtbnd  48607  grtriproplem  48737  grtri  48738  grtrif1o  48740  isgrtri  48741  grimgrtri  48747  usgrexmpl1tri  48823  gpgvtx0  48851  gpgvtx1  48852  gpgedgvtx0  48859  gpgedgvtx1  48860  upwlksfval  48933  isupwlk  48934  el0ldep  49279  ldepspr  49286  lmod1  49305  zlmodzxzldep  49317  catprs  49822  catprsc  49824  prsthinc  50275  2arwcatlem1  50406  cnelsubclem  50414