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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  3anbi12d  1465  3anbi13d  1466  3anbi23d  1467  ax12wdemo  2170  limeq  6372  f13dfv  7272  epne3  7768  oteqimp  8001  xpord2lem  8134  poxp2  8135  xpord3lem  8141  xpord3pred  8144  csbfrecsg  8277  frrlem1  8279  frrlem13  8291  smoeq  8333  on2ind  8651  on3ind  8652  naddasslem1  8677  naddasslem2  8678  naddass  8679  ereq1  8698  sbthfi  9179  indexfi  9313  hartogslem1  9500  brttrcl2  9679  ssttrcl  9680  ttrcltr  9681  ttrclss  9685  ttrclselem2  9691  tz9.1  9694  updjud  9916  alephval3  10090  cofsmo  10248  cfsmolem  10249  alephsing  10255  axdc3lem2  10430  axdc3lem3  10431  axdc3  10433  axdc4lem  10434  zornn0g  10484  fpwwe2lem4  10614  canthwelem  10630  canthwe  10631  pwfseqlem4a  10641  pwfseqlem4  10642  elwina  10666  elina  10667  iswun  10684  elgrug  10772  iccshftr  13508  iccshftl  13510  iccdil  13512  icccntr  13514  fzaddel  13582  elfzomelpfzo  13797  axdc4uzlem  14015  hash3tpb  14528  wrdl1s1  14648  wwlktovf  14989  wwlktovf1  14990  wwlktovfo  14991  wrd2f1tovbij  14993  dfrtrcl2  15095  sqrmo  15298  resqrtcl  15300  resqrtthlem  15301  sqrtneg  15314  sqreu  15408  sqrtthlem  15410  eqsqrtd  15415  prodeq1f  15956  prodeq1  15957  zprod  15987  divalglem10  16455  dfgcd2  16599  coprmprod  16714  pythagtriplem18  16887  pythagtriplem19  16888  prmgaplem3  17108  prmgaplem4  17109  isstruct2  17204  imasval  17560  mreexexlemd  17695  catidd  17731  iscatd2  17732  subsubc  17905  isfunc  17916  funcres2b  17949  ispos  18365  posi  18368  isposd  18373  pospropd  18376  resspos  18480  isps  18619  imasmnd2  18827  sgrp2rid2ex  18984  imasgrp2  19116  psgnunilem3  19561  isrngd  20246  imasrng  20250  isringd  20370  imasring  20408  subrngpropd  20667  isdrngd  20868  isdrngdOLD  20870  islmod  20985  lmodlema  20986  islmodd  20987  lmodprop2d  21045  lmhmpropd  21194  rspprop  21370  isphl  21778  isphld  21804  phlpropd  21805  mdetunilem3  22771  mdetunilem9  22777  fiinopn  23058  iscldtop  23252  lmfval  23389  connsuba  23577  1stcfb  23602  2ndcctbss  23612  subislly  23638  ptval  23727  elpt  23729  elptr  23730  upxp  23780  isfbas  23986  ustval  24360  isust  24361  ustincl  24365  ustdiag  24366  ustinvel  24367  ustexhalf  24368  ust0  24377  imasdsf1olem  24530  tngngp3  24813  lmhmclm  25246  iscph  25329  iscau2  25436  pmltpclem1  25607  isi1f  25833  mbfi1fseqlem6  25879  iblcnlem  25948  dvfsumlem4  26188  aannenlem1  26491  aannenlem2  26492  ulmval  26543  nodense  27856  nosupprefixmo  27864  noinfprefixmo  27865  nosupcbv  27866  nosupfv  27870  noinfcbv  27881  noinffv  27885  noetalem2  27906  eqcuts  27978  no2indlesm  28147  no3inds  28151  addsproplem3  28164  negsproplem3  28223  mulsproplem10  28318  bdayfinbndcbv  28659  bdayfinbndlem1  28660  bdayfinbndlem2  28661  istrkgb  28724  istrkge  28726  istrkgld  28728  istrkg2ld  28729  istrkg3ld  28730  axtgupdim2  28740  axtgeucl  28741  trgcgrg  28784  ishlg2  28871  ishlg  28874  colline  28923  iscgra  29120  isinag  29155  brbtwn  29249  axpaschlem  29290  axlowdim  29311  axeuclid  29313  eengtrkge  29337  issubgr  29621  nb3grpr  29732  nb3grpr2  29733  cplgr3v  29785  wksfval  29959  iswlk  29960  upgr2wlk  30016  wlkiswwlks2  30224  wwlksnextfun  30247  wwlksnextinj  30248  wwlksnextbij  30251  wwlksnextprop  30261  2wlkdlem4  30277  umgr2wlk  30298  usgrwwlks2on  30307  umgrwwlks2on  30308  elwspths2spth  30319  isclwwlk  30335  clwlkclwwlklem1  30350  erclwwlkeq  30369  clwwlkn1loopb  30394  erclwwlkneq  30418  s2elclwwlknon2  30455  3wlkdlem5  30514  3wlkdlem6  30516  3wlkdlem9  30519  3wlkdlem10  30520  uhgr3cyclex  30533  upgr4cycl4dv4e  30536  frgr3v  30626  3cyclfrgrrn1  30636  extwwlkfabel  30704  isplig  30828  lpni  30832  isgrpo  30849  vciOLD  30913  isvclem  30929  isnvlem  30962  sspval  31075  isssp  31076  ajfval  31161  dipdir  31194  siilem2  31204  issh  31560  elunop2  32365  superpos  32706  padct  33063  isslmd  33522  slmdlema  33523  subsdrg  33619  elrspunidl  33736  constrcbvlem  34145  locfinreflem  34230  locfinref  34231  zarcmplem  34271  zhmnrg  34355  ismntoplly  34415  issiga  34502  isrnsiga  34503  isldsys  34546  rossros  34570  ismeas  34589  isrnmeas  34590  pmeasmono  34714  pmeasadd  34715  istrkg2d  35053  axtgupdim2ALTV  35055  afsval  35061  brafs  35062  bnj919  35156  bnj976  35166  bnj607  35304  bnj873  35312  fineqvnttrclse  35537  tz9.1regs  35547  cvmlift3lem2  35812  cvmlift3lem6  35816  cvmlift3lem7  35817  cvmlift3lem9  35819  cvmlift3  35820  mclsppslem  36075  dfon2lem1  36273  dfon2lem3  36275  dfon2lem7  36279  brofs  36497  ofscom  36499  btwnouttr  36516  brifs  36535  cgr3com  36545  brcolinear  36551  brfs  36571  prodeq12sdv  36730  cbvproddavw2  36808  unblimceq0lem  37095  knoppndvlem21  37121  rdgeqoa  38016  poimirlem4  38275  poimirlem27  38298  mblfinlem3  38310  indexa  38384  sdclem1  38394  fdc  38396  neificl  38404  heiborlem2  38463  isass  38497  ismndo2  38525  isrngo  38548  rngomndo  38586  isgrpda  38606  igenval2  38717  eleqvrels2  39325  eleqvrels3  39326  eqvreleq  39335  lshpset2N  39893  isopos  39954  oposlem  39956  cmtfvalN  39984  cvrfval  40042  3dimlem1  40232  3dim1lem5  40240  lplni2  40311  lvoli2  40355  4atlem11  40383  dalawlem15  40659  cdlemftr3  41339  tendofset  41532  tendoset  41533  istendo  41534  cdlemk28-3  41682  cdlemkid3N  41707  cdlemkid4  41708  lpolsetN  42256  islpolN  42257  lpolconN  42261  isprimroot  42860  aks6d1c1p1  42874  ismrc  43432  rabren3dioph  43542  irrapxlem5  43553  rmydioph  43741  mpaaeu  43877  mpaaval  43878  mpaalem  43879  naddwordnexlem4  44128  dfsucon  44249  minregex  44260  dfrtrcl3  44459  brco3f1o  44759  grumnud  44996  modelaxreplem1  45687  modelaxreplem2  45688  modelaxrep  45690  eliooshift  46222  stoweidlem5  46719  stoweidlem18  46732  stoweidlem28  46742  stoweidlem31  46745  stoweidlem41  46755  stoweidlem43  46757  stoweidlem44  46758  stoweidlem45  46759  stoweidlem51  46765  stoweidlem55  46769  stoweidlem59  46773  issal  47028  fundcmpsurbijinjpreimafv  48156  fundcmpsurbijinj  48159  fundcmpsurinjALT  48161  ichnreuop  48221  proththdlem  48365  6gbe  48536  8gbe  48538  bgoldbtbndlem2  48571  bgoldbtbndlem3  48572  bgoldbtbnd  48574  grtriproplem  48704  grtri  48705  grtrif1o  48707  isgrtri  48708  grimgrtri  48714  usgrexmpl1tri  48790  gpgvtx0  48818  gpgvtx1  48819  gpgedgvtx0  48826  gpgedgvtx1  48827  upwlksfval  48900  isupwlk  48901  el0ldep  49246  ldepspr  49253  lmod1  49272  zlmodzxzldep  49284  catprs  49789  catprsc  49791  prsthinc  50242  2arwcatlem1  50373  cnelsubclem  50381