Theorem 3anbi123d 1437

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  3anbi12d  1438  3anbi13d  1439  3anbi23d  1440  ax12wdemo  2132  limeq  6374  f13dfv  7269  epne3  7757  oteqimp  7991  xpord2lem  8125  poxp2  8126  xpord3lem  8132  xpord3pred  8135  csbfrecsg  8266  frrlem1  8268  frrlem13  8280  wfrlem1OLD  8305  wfrlem15OLD  8320  smoeq  8347  on2ind  8665  on3ind  8666  naddasslem1  8690  naddasslem2  8691  naddass  8692  ereq1  8707  sbthfi  9199  indexfi  9357  hartogslem1  9534  brttrcl2  9706  ssttrcl  9707  ttrcltr  9708  ttrclss  9712  ttrclselem2  9718  tz9.1  9721  updjud  9926  alephval3  10102  cofsmo  10261  cfsmolem  10262  alephsing  10268  axdc3lem2  10443  axdc3lem3  10444  axdc3  10446  axdc4lem  10447  zornn0g  10497  fpwwe2lem4  10626  canthwelem  10642  canthwe  10643  pwfseqlem4a  10653  pwfseqlem4  10654  elwina  10678  elina  10679  iswun  10696  elgrug  10784  iccshftr  13460  iccshftl  13462  iccdil  13464  icccntr  13466  fzaddel  13532  elfzomelpfzo  13733  axdc4uzlem  13945  wrdl1s1  14561  wwlktovf  14904  wwlktovf1  14905  wwlktovfo  14906  wrd2f1tovbij  14908  dfrtrcl2  15006  sqrmo  15195  resqrtcl  15197  resqrtthlem  15198  sqrtneg  15211  sqreu  15304  sqrtthlem  15306  eqsqrtd  15311  prodeq1f  15849  zprod  15878  divalglem10  16342  dfgcd2  16485  coprmprod  16595  pythagtriplem18  16762  pythagtriplem19  16763  prmgaplem3  16983  prmgaplem4  16984  isstruct2  17079  imasval  17454  mreexexlemd  17585  catidd  17621  iscatd2  17622  subsubc  17800  isfunc  17811  funcres2b  17844  ispos  18264  posi  18267  isposd  18273  pospropd  18277  isps  18518  imasmnd2  18659  sgrp2rid2ex  18805  imasgrp2  18935  psgnunilem3  19359  isringd  20099  imasring  20137  isdrngd  20341  isdrngdOLD  20343  islmod  20468  lmodlema  20469  islmodd  20470  lmodprop2d  20527  lmhmpropd  20677  isphl  21173  isphld  21199  phlpropd  21200  mdetunilem3  22108  mdetunilem9  22114  fiinopn  22395  iscldtop  22591  lmfval  22728  connsuba  22916  1stcfb  22941  2ndcctbss  22951  subislly  22977  ptval  23066  elpt  23068  elptr  23069  upxp  23119  isfbas  23325  ustval  23699  isust  23700  ustincl  23704  ustdiag  23705  ustinvel  23706  ustexhalf  23707  ust0  23716  imasdsf1olem  23871  tngngp3  24165  lmhmclm  24595  iscph  24679  iscau2  24786  pmltpclem1  24957  isi1f  25183  mbfi1fseqlem6  25230  iblcnlem  25298  dvfsumlem4  25538  aannenlem1  25833  aannenlem2  25834  ulmval  25884  nodense  27185  nosupprefixmo  27193  noinfprefixmo  27194  nosupcbv  27195  nosupfv  27199  noinfcbv  27210  noinffv  27214  noetalem2  27235  eqscut  27296  no2indslem  27428  no3inds  27432  addsproplem3  27445  negsproplem3  27494  mulsproplem10  27571  istrkgb  27696  istrkge  27698  istrkgld  27700  istrkg2ld  27701  istrkg3ld  27702  axtgupdim2  27712  axtgeucl  27713  trgcgrg  27756  ishlg  27843  colline  27890  iscgra  28050  isinag  28079  brbtwn  28147  axpaschlem  28188  axlowdim  28209  axeuclid  28211  eengtrkge  28235  issubgr  28518  nb3grpr  28629  nb3grpr2  28630  cplgr3v  28682  wksfval  28856  iswlk  28857  upgr2wlk  28915  wlkiswwlks2  29119  wwlksnextfun  29142  wwlksnextinj  29143  wwlksnextbij  29146  wwlksnextprop  29156  2wlkdlem4  29172  umgr2wlk  29193  umgrwwlks2on  29201  elwspths2spth  29211  isclwwlk  29227  clwlkclwwlklem1  29242  erclwwlkeq  29261  clwwlkn1loopb  29286  erclwwlkneq  29310  s2elclwwlknon2  29347  3wlkdlem5  29406  3wlkdlem6  29408  3wlkdlem9  29411  3wlkdlem10  29412  uhgr3cyclex  29425  upgr4cycl4dv4e  29428  frgr3v  29518  3cyclfrgrrn1  29528  extwwlkfabel  29596  isplig  29717  lpni  29721  isgrpo  29738  vciOLD  29802  isvclem  29818  isnvlem  29851  sspval  29964  isssp  29965  ajfval  30050  dipdir  30083  siilem2  30093  issh  30449  elunop2  31254  superpos  31595  padct  31932  resspos  32124  isslmd  32335  slmdlema  32336  elrspunidl  32535  locfinreflem  32809  locfinref  32810  zarcmplem  32850  zhmnrg  32936  ismntoplly  32994  issiga  33099  isrnsiga  33100  isldsys  33143  rossros  33167  ismeas  33186  isrnmeas  33187  pmeasmono  33312  pmeasadd  33313  istrkg2d  33667  axtgupdim2ALTV  33669  afsval  33672  brafs  33673  bnj919  33767  bnj976  33777  bnj607  33916  bnj873  33924  cvmlift3lem2  34300  cvmlift3lem6  34304  cvmlift3lem7  34305  cvmlift3lem9  34307  cvmlift3  34308  mclsppslem  34563  dfon2lem1  34744  dfon2lem3  34746  dfon2lem7  34750  brofs  34966  ofscom  34968  btwnouttr  34985  brifs  35004  cgr3com  35014  brcolinear  35020  brfs  35040  unblimceq0lem  35371  knoppndvlem21  35397  rdgeqoa  36240  poimirlem4  36481  poimirlem27  36504  mblfinlem3  36516  indexa  36590  sdclem1  36600  fdc  36602  neificl  36610  heiborlem2  36669  isass  36703  ismndo2  36731  isrngo  36754  rngomndo  36792  isgrpda  36812  igenval2  36923  eleqvrels2  37451  eleqvrels3  37452  eqvreleq  37461  lshpset2N  37978  isopos  38039  oposlem  38041  cmtfvalN  38069  cvrfval  38127  3dimlem1  38318  3dim1lem5  38326  lplni2  38397  lvoli2  38441  4atlem11  38469  dalawlem15  38745  cdlemftr3  39425  tendofset  39618  tendoset  39619  istendo  39620  cdlemk28-3  39768  cdlemkid3N  39793  cdlemkid4  39794  lpolsetN  40342  islpolN  40343  lpolconN  40347  ismrc  41425  rabren3dioph  41539  irrapxlem5  41550  rmydioph  41739  mpaaeu  41878  mpaaval  41879  mpaalem  41880  naddwordnexlem4  42138  dfsucon  42260  minregex  42271  dfrtrcl3  42470  brco3f1o  42770  grumnud  43031  eliooshift  44206  stoweidlem5  44708  stoweidlem18  44721  stoweidlem28  44731  stoweidlem31  44734  stoweidlem41  44744  stoweidlem43  44746  stoweidlem44  44747  stoweidlem45  44748  stoweidlem51  44754  stoweidlem55  44758  stoweidlem59  44762  issal  45017  fundcmpsurbijinjpreimafv  46062  fundcmpsurbijinj  46065  fundcmpsurinjALT  46067  ichnreuop  46127  proththdlem  46268  6gbe  46426  8gbe  46428  bgoldbtbndlem2  46461  bgoldbtbndlem3  46462  bgoldbtbnd  46464  upwlksfval  46500  isupwlk  46501  isrngd  46659  imasrng  46665  subrngpropd  46732  el0ldep  47101  ldepspr  47108  lmod1  47127  zlmodzxzldep  47139  catprs  47585  catprsc  47587  prsthinc  47628