Theorem 3anbi123d 1434

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  3anbi12d  1435  3anbi13d  1436  3anbi23d  1437  ax12wdemo  2133  limeq  6263  f13dfv  7127  epne3  7601  oteqimp  7823  csbfrecsg  8071  frrlem1  8073  frrlem13  8085  wfrlem1OLD  8110  wfrlem15OLD  8125  smoeq  8152  ereq1  8463  sbthfi  8942  indexfi  9057  hartogslem1  9231  tz9.1  9418  updjud  9623  alephval3  9797  cofsmo  9956  cfsmolem  9957  alephsing  9963  axdc3lem2  10138  axdc3lem3  10139  axdc3  10141  axdc4lem  10142  zornn0g  10192  fpwwe2lem4  10321  canthwelem  10337  canthwe  10338  pwfseqlem4a  10348  pwfseqlem4  10349  elwina  10373  elina  10374  iswun  10391  elgrug  10479  iccshftr  13147  iccshftl  13149  iccdil  13151  icccntr  13153  fzaddel  13219  elfzomelpfzo  13419  axdc4uzlem  13631  wrdl1s1  14247  wwlktovf  14599  wwlktovf1  14600  wwlktovfo  14601  wrd2f1tovbij  14603  dfrtrcl2  14701  sqrmo  14891  resqrtcl  14893  resqrtthlem  14894  sqrtneg  14907  sqreu  15000  sqrtthlem  15002  eqsqrtd  15007  prodeq1f  15546  zprod  15575  divalglem10  16039  dfgcd2  16182  coprmprod  16294  pythagtriplem18  16461  pythagtriplem19  16462  prmgaplem3  16682  prmgaplem4  16683  isstruct2  16778  imasval  17139  mreexexlemd  17270  catidd  17306  iscatd2  17307  subsubc  17484  isfunc  17495  funcres2b  17528  ispos  17947  posi  17950  isposd  17956  pospropd  17960  isps  18201  imasmnd2  18337  sgrp2rid2ex  18481  imasgrp2  18605  psgnunilem3  19019  isringd  19739  imasring  19773  isdrngd  19931  islmod  20042  lmodlema  20043  islmodd  20044  lmodprop2d  20100  lmhmpropd  20250  isphl  20745  isphld  20771  phlpropd  20772  assapropd  20986  mdetunilem3  21671  mdetunilem9  21677  fiinopn  21958  iscldtop  22154  lmfval  22291  connsuba  22479  1stcfb  22504  2ndcctbss  22514  subislly  22540  ptval  22629  elpt  22631  elptr  22632  upxp  22682  isfbas  22888  ustval  23262  isust  23263  ustincl  23267  ustdiag  23268  ustinvel  23269  ustexhalf  23270  ust0  23279  imasdsf1olem  23434  tngngp3  23726  lmhmclm  24156  iscph  24239  iscau2  24346  pmltpclem1  24517  isi1f  24743  mbfi1fseqlem6  24790  iblcnlem  24858  dvfsumlem4  25098  aannenlem1  25393  aannenlem2  25394  ulmval  25444  istrkgb  26720  istrkge  26722  istrkgld  26724  istrkg2ld  26725  istrkg3ld  26726  axtgupdim2  26736  axtgeucl  26737  trgcgrg  26780  ishlg  26867  colline  26914  iscgra  27074  isinag  27103  brbtwn  27170  axpaschlem  27211  axlowdim  27232  axeuclid  27234  eengtrkge  27258  issubgr  27541  nb3grpr  27652  nb3grpr2  27653  cplgr3v  27705  wksfval  27879  iswlk  27880  upgr2wlk  27938  wlkiswwlks2  28141  wwlksnextfun  28164  wwlksnextinj  28165  wwlksnextbij  28168  wwlksnextprop  28178  2wlkdlem4  28194  umgr2wlk  28215  umgrwwlks2on  28223  elwspths2spth  28233  isclwwlk  28249  clwlkclwwlklem1  28264  erclwwlkeq  28283  clwwlkn1loopb  28308  erclwwlkneq  28332  s2elclwwlknon2  28369  3wlkdlem5  28428  3wlkdlem6  28430  3wlkdlem9  28433  3wlkdlem10  28434  uhgr3cyclex  28447  upgr4cycl4dv4e  28450  frgr3v  28540  3cyclfrgrrn1  28550  extwwlkfabel  28618  isplig  28739  lpni  28743  isgrpo  28760  vciOLD  28824  isvclem  28840  isnvlem  28873  sspval  28986  isssp  28987  ajfval  29072  dipdir  29105  siilem2  29115  issh  29471  elunop2  30276  superpos  30617  padct  30956  resspos  31146  isslmd  31357  slmdlema  31358  elrspunidl  31508  locfinreflem  31692  locfinref  31693  zarcmplem  31733  zhmnrg  31817  ismntoplly  31875  issiga  31980  isrnsiga  31981  isldsys  32024  rossros  32048  ismeas  32067  isrnmeas  32068  pmeasmono  32191  pmeasadd  32192  istrkg2d  32546  axtgupdim2ALTV  32548  afsval  32551  brafs  32552  bnj919  32647  bnj976  32657  bnj607  32796  bnj873  32804  cvmlift3lem2  33182  cvmlift3lem6  33186  cvmlift3lem7  33187  cvmlift3lem9  33189  cvmlift3  33190  mclsppslem  33445  dfon2lem1  33665  dfon2lem3  33667  dfon2lem7  33671  brttrcl2  33700  ssttrcl  33701  ttrcltr  33702  ttrclss  33706  ttrclselem2  33712  xpord2lem  33716  poxp2  33717  xpord3lem  33722  xpord3pred  33725  on2ind  33755  on3ind  33756  nodense  33822  nosupprefixmo  33830  noinfprefixmo  33831  nosupcbv  33832  nosupfv  33836  noinfcbv  33847  noinffv  33851  noetalem2  33872  eqscut  33926  no2indslem  34038  no3inds  34042  brofs  34234  ofscom  34236  btwnouttr  34253  brifs  34272  cgr3com  34282  brcolinear  34288  brfs  34308  unblimceq0lem  34613  knoppndvlem21  34639  rdgeqoa  35468  poimirlem4  35708  poimirlem27  35731  mblfinlem3  35743  indexa  35818  sdclem1  35828  fdc  35830  neificl  35838  heiborlem2  35897  isass  35931  ismndo2  35959  isrngo  35982  rngomndo  36020  isgrpda  36040  igenval2  36151  eleqvrels2  36632  eleqvrels3  36633  eqvreleq  36642  lshpset2N  37060  isopos  37121  oposlem  37123  cmtfvalN  37151  cvrfval  37209  3dimlem1  37399  3dim1lem5  37407  lplni2  37478  lvoli2  37522  4atlem11  37550  dalawlem15  37826  cdlemftr3  38506  tendofset  38699  tendoset  38700  istendo  38701  cdlemk28-3  38849  cdlemkid3N  38874  cdlemkid4  38875  lpolsetN  39423  islpolN  39424  lpolconN  39428  ismrc  40439  rabren3dioph  40553  irrapxlem5  40564  rmydioph  40752  mpaaeu  40891  mpaaval  40892  mpaalem  40893  dfsucon  41028  dfrtrcl3  41230  brco3f1o  41532  grumnud  41793  eliooshift  42934  stoweidlem5  43436  stoweidlem18  43449  stoweidlem28  43459  stoweidlem31  43462  stoweidlem41  43472  stoweidlem43  43474  stoweidlem44  43475  stoweidlem45  43476  stoweidlem51  43482  stoweidlem55  43486  stoweidlem59  43490  issal  43745  fundcmpsurbijinjpreimafv  44747  fundcmpsurbijinj  44750  fundcmpsurinjALT  44752  ichnreuop  44812  proththdlem  44953  6gbe  45111  8gbe  45113  bgoldbtbndlem2  45146  bgoldbtbndlem3  45147  bgoldbtbnd  45149  upwlksfval  45185  isupwlk  45186  el0ldep  45695  ldepspr  45702  lmod1  45721  zlmodzxzldep  45733  catprs  46180  catprsc  46182  prsthinc  46223