Theorem anbi12d 473

Description: Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
anbi12d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
anbi12d.2	⊢ (𝜑 → (𝜃 ↔ 𝜏))

Assertion

Ref	Expression
anbi12d	⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜏)))

Proof of Theorem anbi12d

Step	Hyp	Ref	Expression
1		anbi12d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	anbi1d 465	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜃)))
3		anbi12d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	3	anbi2d 464	. 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜃) ↔ (𝜒 ∧ 𝜏)))
5	2, 4	bitrd 188	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜏)))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm4.38  609  pm5.17dc  912  orbididc  962  ifpbi123d  1001  3anbi123d  1349  xorbi2d  1425  xorbi1d  1426  drsb1  1847  mopick  2158  clelab  2358  cbvrmow  2717  cbvrexfw  2758  cbvrexf  2760  cbvreu  2766  cbvrexvw  2773  cbvreuvw  2774  cbvrexdva2  2776  cbvrab  2801  gencbvex  2851  rspce  2906  eqvincf  2932  ceqsrexv  2937  elrabf  2961  rexab2  2973  reu2  2995  reu6  2996  rmo4  3000  reu8  3003  reuind  3012  sbcan  3075  sbcang  3076  reu8nf  3114  sbcabel  3115  rmob  3126  cbvrexcsf  3192  cbvreucsf  3193  cbvrabcsf  3194  difjust  3202  injust  3206  eldif  3210  ssconb  3342  elin  3392  opeq1  3867  opeq2  3868  2ralunsn  3887  elunii  3903  csbunig  3906  eluniab  3910  cbvopab  4165  cbvopab1  4167  cbvopab2  4168  cbvopab1s  4169  cbvopab2v  4171  cbvmptf  4188  cbvmpt  4189  trel  4199  nalset  4224  elssabg  4243  mss  4324  exss  4325  opelopab2a  4365  poeq1  4402  pocl  4406  soeq1  4418  weeq1  4459  weeq2  4460  ordeq  4475  zfun  4537  snnex  4551  reusv3  4563  ontr2exmid  4629  regexmid  4639  onintexmid  4677  reg3exmid  4684  peano5  4702  limom  4718  nnregexmid  4725  vtoclr  4780  opeliunxp  4787  poinxp  4801  opbrop  4811  csbxpg  4813  opeliunxp2  4876  relop  4886  brcogw  4905  elrnmpt1  4989  elsnres  5056  dfres2  5071  inimasn  5161  xpcanm  5183  xpcan2m  5184  elxp4  5231  elxp5  5232  cnvsom  5287  sbcfung  5357  funopg  5367  fununi  5405  funcnvuni  5406  fneq1  5425  2elresin  5450  feq1  5472  sbcfng  5487  sbcfg  5488  f1eq1  5546  foeq1  5564  f1oeq1  5580  f1oeq2  5581  f1oeq3  5582  ffoss  5625  brprcneu  5641  fv3  5671  tz6.12f  5677  ssimaex  5716  fvopab3g  5728  fvopab3ig  5729  fvopab6  5752  fmptco  5821  fsn2g  5830  funopsn  5838  funopdmsn  5842  elunirn  5917  f1imaeq  5926  foeqcnvco  5941  fliftfun  5947  fliftval  5951  isoeq1  5952  isoeq4  5955  isoini  5969  isopolem  5973  f1oiso2  5978  riotabidv  5983  cbvriotavw  5992  cbvriota  5993  acexmid  6027  ovanraleqv  6052  cbvoprab1  6103  cbvoprab2  6104  cbvoprab12  6105  cbvmpox  6109  ov  6151  ovig  6153  ovg  6171  caovimo  6226  caoftrn  6277  opabex3d  6292  opabex3  6293  uchoice  6309  elxp6  6341  unielxp  6346  dfoprab4  6364  dfoprab4f  6365  fmpox  6374  xporderlem  6405  poxp  6406  cnvoprab  6408  f1od2  6409  opeliunxp2f  6447  rbropapd  6451  dftpos4  6472  tpostpos  6473  smoiso  6511  tfrlem3ag  6518  tfrlem3a  6519  tfr0dm  6531  tfrlemisucaccv  6534  tfrlemiex  6540  tfrlemi1  6541  tfrlemi14d  6542  tfrexlem  6543  tfr1onlem3ag  6546  tfr1onlemsucaccv  6550  tfr1onlemex  6556  tfr1onlemaccex  6557  tfr1onlemres  6558  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllemex  6569  tfrcllemaccex  6570  tfrcllemres  6571  tfrcldm  6572  frec0g  6606  frecabcl  6608  freccllem  6611  frecfcllem  6613  frecsuclem  6615  frecsuc  6616  nnacan  6723  nnmcan  6730  nnaordex  6739  ertr  6760  brecop  6837  eroveu  6838  ecopovtrn  6844  ecopovtrng  6847  th3qlem1  6849  th3qlem2  6850  th3q  6852  elpm2r  6878  mapsncnv  6907  elixp2  6914  ixpeq1  6921  elixpsn  6947  ixpsnf1o  6948  mapsnen  7029  map1  7030  xpsnen  7048  endisj  7051  pw2f1odclem  7063  xpf1o  7073  phplem3g  7085  ssfiexmid  7106  ssfiexmidt  7108  domfiexmid  7110  findcard2s  7122  isinfinf  7129  ac6sfi  7130  fiintim  7166  fisseneq  7170  opabfi  7175  f1dmvrnfibi  7186  sbthlem2  7200  isbth  7209  supeq1  7228  supeq3  7232  supeq123d  7233  supmoti  7235  eqsupti  7238  supsnti  7247  isotilem  7248  isoti  7249  supisolem  7250  supisoex  7251  cnvinfex  7260  cnvti  7261  eqinfti  7262  infvalti  7264  updjud  7324  ctssexmid  7392  omniwomnimkv  7409  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  acneq  7460  acfun  7465  tapeq1  7514  tapeq2  7515  exmidapne  7522  ccfunen  7526  cc2lem  7528  cc3  7530  ltsopi  7583  recexnq  7653  recmulnqg  7654  ltsonq  7661  lt2addnq  7667  lt2mulnq  7668  ltbtwnnqq  7678  prarloclemarch2  7682  enq0sym  7695  enq0ref  7696  enq0tr  7697  enq0breq  7699  addnq0mo  7710  mulnq0mo  7711  addnnnq0  7712  mulnnnq0  7713  nqnq0a  7717  nqnq0m  7718  elinp  7737  prcdnql  7747  prcunqu  7748  prltlu  7750  prdisj  7755  prarloclemlo  7757  prarloclem3  7760  prarloclem5  7763  ltdfpr  7769  genprndl  7784  genprndu  7785  genpdisj  7786  appdivnq  7826  ltpopr  7858  ltexprlemdisj  7869  ltexprlemloc  7870  ltexprlemrl  7873  ltexprlemru  7875  ltexpri  7876  recexprlemm  7887  recexprlemdisj  7893  recexprlemloc  7894  recexprlem1ssl  7896  recexprlem1ssu  7897  recexpr  7901  aptiprleml  7902  archpr  7906  cauappcvgprlemladdru  7919  cauappcvgprlemladdrl  7920  cauappcvgprlem1  7922  cauappcvgprlemlim  7924  cauappcvgpr  7925  caucvgprlemnkj  7929  caucvgprlemnbj  7930  caucvgprlemcl  7939  caucvgpr  7945  caucvgprprlemcbv  7950  caucvgprprlemval  7951  caucvgprprlemopu  7962  caucvgprpr  7975  suplocexpr  7988  addsrmo  8006  mulsrmo  8007  addsrpr  8008  mulsrpr  8009  lttrsr  8025  recexgt0sr  8036  caucvgsrlemcau  8056  caucvgsrlemgt1  8058  caucvgsrlemoffcau  8061  caucvgsrlemoffres  8063  caucvgsr  8065  suplocsrlem  8071  ltresr  8102  pitonn  8111  peano1nnnn  8115  peano2nnnn  8116  axprecex  8143  axcnre  8144  axpre-lttrn  8147  peano5nnnn  8155  axcaucvglemcau  8161  axcaucvglemres  8162  axpre-suploclemres  8164  axpre-suploc  8165  axlttrn  8290  axsuploc  8294  letri3  8302  letr  8304  le2add  8666  lt2add  8667  ltleadd  8668  lt2sub  8682  le2sub  8683  apreap  8809  apreim  8825  apti  8844  msq11  9124  dfinfre  9178  sup3exmid  9179  cju  9183  peano5nni  9188  1nn  9196  peano2nn  9197  nn2ge  9218  nominpos  9424  elz2  9595  dfuzi  9634  uzind  9635  supinfneg  9873  infsupneg  9874  elpqb  9928  xrletri3  10083  xrletr  10087  z2ge  10105  elixx1  10176  elioo2  10200  iooshf  10231  iooneg  10267  iccneg  10268  icoshft  10269  elfz1  10293  fzdifsuc  10361  fzrev  10364  1fv  10419  zsupcllemstep  10535  infssuzex  10539  nninfdcex  10543  zsupssdc  10544  exbtwnzlemstep  10553  exbtwnzlemshrink  10554  exbtwnzlemex  10555  exbtwnz  10556  rebtwn2zlemstep  10558  rebtwn2zlemshrink  10559  rebtwn2z  10560  qbtwnre  10562  qbtwnxr  10563  flval  10578  flqlelt  10582  flqbi  10596  flqbi2  10597  modqid2  10659  q2submod  10693  seqf1og  10829  nnesq  10967  hashunlem  11113  zfz1isolem1  11150  zfz1iso  11151  seq3coll  11152  fundm2domnop0  11158  pfxsuffeqwrdeq  11328  swrdpfx  11337  wrd2ind  11353  swrdccatin2  11359  swrdccatin2d  11374  pfxccatin12d  11375  reuccatpfxs1lem  11376  reuccatpfxs1  11377  shftlem  11439  shftfibg  11443  shftfib  11446  shftfn  11447  2shfti  11454  cjval  11468  cjth  11469  remim  11483  caucvgrelemcau  11603  caucvgre  11604  cvg1nlemcau  11607  cvg1nlemres  11608  rexanuz2  11614  recvguniq  11618  resqrexlemgt0  11643  resqrexlemoverl  11644  resqrexlemglsq  11645  resqrexlemsqa  11647  resqrexlemex  11648  rsqrmo  11650  resqrtcl  11652  rersqrtthlem  11653  absdiflt  11715  absdifle  11716  cau3lem  11737  icodiamlt  11803  maxleast  11836  negfi  11851  minmax  11853  lemininf  11857  ltmininf  11858  xrmaxlesup  11882  xrminmax  11888  xrltmininf  11893  xrlemininf  11894  iooinsup  11900  clim  11904  clim2  11906  climshftlemg  11925  addcn2  11933  climcau  11970  summodc  12007  fsum3  12011  fsum2dlemstep  12058  fisumcom2  12062  fsum00  12086  ntrivcvgap0  12173  prodeq1f  12176  prodeq2w  12180  prodeq2  12181  prodmodc  12202  zproddc  12203  fprodseq  12207  fprodntrivap  12208  fprod2dlemstep  12246  fprodcom2fi  12250  sin01bnd  12381  cos01bnd  12382  divalgmod  12551  ndvdssub  12554  gcdsupex  12591  gcdsupcl  12592  gcddvds  12597  dvdslegcd  12598  bezoutlemmain  12632  bezoutlemex  12635  bezoutlemzz  12636  bezoutlemeu  12641  bezoutlemle  12642  bezoutlemsup  12643  dfgcd3  12644  dfgcd2  12648  gcddiv  12653  lcmval  12698  lcmcllem  12702  dvdslcm  12704  lcmledvds  12705  lcmgcdlem  12712  lcmdvds  12714  coprmgcdb  12723  ncoprmgcdne1b  12724  coprmdvds1  12726  qredeu  12732  divgcdcoprm0  12736  divgcdcoprmex  12737  isprm3  12753  pw2dvdslemn  12800  pw2dvdseu  12803  oddpwdclemxy  12804  qnumdencl  12822  qnumdenbi  12827  crth  12859  reumodprminv  12889  pythagtriplem19  12918  pceu  12931  pczpre  12933  pcdiv  12938  pc11  12967  dvdsprmpweqle  12973  prmpwdvds  12991  pockthi  12994  infpnlem2  12996  elgz  13007  4sqlem12  13038  ennnfonelemim  13108  exmidunben  13110  ctinfom  13112  ctiunctlemu1st  13118  ctiunctlemu2nd  13119  ctiunctlemudc  13121  ctiunctlemfo  13123  infpn2  13140  ptex  13410  prdsval  13419  f1ocpbllem  13456  ercpbl  13477  erlecpbl  13478  grpidvalg  13519  grpidpropdg  13520  mgmlrid  13525  igsumvalx  13535  gsumfzval  13537  gsumress  13541  gsumval2  13543  issgrpd  13558  sgrppropd  13559  ismnddef  13564  sgrpidmndm  13566  ismndd  13583  mndpropd  13586  mndinvmod  13591  mnd1  13601  ismhm  13607  mhmex  13608  mhmpropd  13612  issubm  13618  insubm  13631  grppropd  13663  dfgrp2  13673  isgrpid2  13686  isgrpinv  13700  grplrinv  13703  grpidinv2  13704  grpidinv  13705  dfgrp3mlem  13744  grplactcnv  13748  releqgg  13870  eqgex  13871  eqgfval  13872  eqgval  13873  isghm  13893  ghmrn  13907  resghm  13910  ghmpropd  13933  cmnpropd  13945  ablpropd  13946  imasabl  13986  isrng  14011  rngdi  14017  rngdir  14018  rngpropd  14032  dfur2g  14039  issrg  14042  srgideu  14049  srgidmlem  14055  issrgid  14058  srg1zr  14064  isring  14077  ringideu  14094  ringidmlem  14099  isringid  14102  ringid  14103  ringpropd  14115  ring1  14136  oppr0g  14158  oppr1g  14159  dvdsrvald  14171  dvdsrd  14172  dvdsrtr  14179  unitgrp  14194  dvdsrpropdg  14225  unitpropdg  14226  rhmopp  14254  opprnzrbg  14263  opprsubrngg  14289  issubrg  14299  subrg1  14309  subrgugrp  14318  resrhm2b  14327  subrgpropd  14331  rhmpropd  14332  opprdomnbg  14353  aprval  14361  aprap  14365  islmod  14370  lmodlema  14371  islmodd  14372  lmodfopnelem2  14404  lmodprop2d  14427  islssm  14436  islssmg  14437  rnglidlrng  14577  isridl  14583  df2idl2rng  14587  quscrng  14612  istopg  14793  fiinbas  14843  eltg2  14847  topbas  14861  neiint  14939  neipsm  14948  opnneissb  14949  opnssneib  14950  innei  14957  restbasg  14962  iscnp4  15012  cnpnei  15013  cnconst2  15027  cnptopresti  15032  cnptoprest  15033  cnpdis  15036  lmss  15040  lmres  15042  txbas  15052  eltx  15053  neitx  15062  txcnp  15065  txcnmpt  15067  uptx  15068  txdis  15071  txdis1cn  15072  txlm  15073  txhmeo  15113  ispsmet  15117  ismet  15138  isxmet  15139  bldisj  15195  blininf  15218  blssexps  15223  blssex  15224  ssblex  15225  xmspropd  15271  mspropd  15272  neibl  15285  metequiv  15289  bdmopn  15298  metrest  15300  xmetxp  15301  xmetxpbl  15302  xmettx  15304  metcnp3  15305  tgioo  15348  tgqioo  15349  addcncntoplem  15355  mpomulcn  15360  mulcncflem  15401  dedekindeu  15417  dedekindicclemicc  15426  limccl  15453  ellimc3apf  15454  limcimolemlt  15458  limccoap  15472  elply2  15529  sin0pilem2  15576  sincosq1sgn  15620  sincosq2sgn  15621  sincosq3sgn  15622  sincosq4sgn  15623  pellexlem3  15776  perfect  15798  lgsval  15806  lgsdir2lem5  15834  lgsne0  15840  lgsquadlem1  15879  lgsquadlem2  15880  lgsquadlem3  15881  lgsquad  15882  2lgslem3  15903  2sqlem8a  15924  2sqlem8  15925  2sqlem9  15926  gropd  15971  grstructd2dom  15972  incistruhgr  16014  uhgr2edg  16130  vtxd0nedgbfi  16223  wlkeq  16278  istrl  16309  clwwlkn2  16345  eupthsg  16369  iseupth  16371  eupth2lem1  16382  depind  16433  bj-sseq  16493  bj-charfunbi  16510  bj-nalset  16594  bj-indeq  16628  bj-2inf  16637  strcoll2  16682  strcollnft  16683  strcollnfALT  16685  sscoll2  16687  subctctexmid  16705  domomsubct  16706  exmidsbthrlem  16733  sbthom  16737  qdencn  16738  qdiff  16764  ltlenmkv  16786  gfsumval  16792