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  911  orbididc  961  ifpbi123d  1000  3anbi123d  1348  xorbi2d  1424  xorbi1d  1425  drsb1  1847  mopick  2158  clelab  2357  cbvrmow  2716  cbvrexfw  2757  cbvrexf  2759  cbvreu  2765  cbvrexvw  2772  cbvreuvw  2773  cbvrexdva2  2775  cbvrab  2800  gencbvex  2850  rspce  2905  eqvincf  2931  ceqsrexv  2936  elrabf  2960  rexab2  2972  reu2  2994  reu6  2995  rmo4  2999  reu8  3002  reuind  3011  sbcan  3074  sbcang  3075  reu8nf  3113  sbcabel  3114  rmob  3125  cbvrexcsf  3191  cbvreucsf  3192  cbvrabcsf  3193  difjust  3201  injust  3205  eldif  3209  ssconb  3340  elin  3390  opeq1  3862  opeq2  3863  2ralunsn  3882  elunii  3898  csbunig  3901  eluniab  3905  cbvopab  4160  cbvopab1  4162  cbvopab2  4163  cbvopab1s  4164  cbvopab2v  4166  cbvmptf  4183  cbvmpt  4184  trel  4194  nalset  4219  elssabg  4238  mss  4318  exss  4319  opelopab2a  4359  poeq1  4396  pocl  4400  soeq1  4412  weeq1  4453  weeq2  4454  ordeq  4469  zfun  4531  snnex  4545  reusv3  4557  ontr2exmid  4623  regexmid  4633  onintexmid  4671  reg3exmid  4678  peano5  4696  limom  4712  nnregexmid  4719  vtoclr  4774  opeliunxp  4781  poinxp  4795  opbrop  4805  csbxpg  4807  opeliunxp2  4870  relop  4880  brcogw  4899  elrnmpt1  4983  elsnres  5050  dfres2  5065  inimasn  5154  xpcanm  5176  xpcan2m  5177  elxp4  5224  elxp5  5225  cnvsom  5280  sbcfung  5350  funopg  5360  fununi  5398  funcnvuni  5399  fneq1  5418  2elresin  5443  feq1  5465  sbcfng  5480  sbcfg  5481  f1eq1  5537  foeq1  5555  f1oeq1  5571  f1oeq2  5572  f1oeq3  5573  ffoss  5616  brprcneu  5632  fv3  5662  tz6.12f  5668  ssimaex  5707  fvopab3g  5719  fvopab3ig  5720  fvopab6  5743  fmptco  5813  fsn2g  5822  funopsn  5830  funopdmsn  5834  elunirn  5907  f1imaeq  5916  foeqcnvco  5931  fliftfun  5937  fliftval  5941  isoeq1  5942  isoeq4  5945  isoini  5959  isopolem  5963  f1oiso2  5968  riotabidv  5973  cbvriotavw  5982  cbvriota  5983  acexmid  6017  ovanraleqv  6042  cbvoprab1  6093  cbvoprab2  6094  cbvoprab12  6095  cbvmpox  6099  ov  6141  ovig  6143  ovg  6161  caovimo  6216  caoftrn  6268  opabex3d  6283  opabex3  6284  uchoice  6300  elxp6  6332  unielxp  6337  dfoprab4  6355  dfoprab4f  6356  fmpox  6365  xporderlem  6396  poxp  6397  cnvoprab  6399  f1od2  6400  opeliunxp2f  6404  rbropapd  6408  dftpos4  6429  tpostpos  6430  smoiso  6468  tfrlem3ag  6475  tfrlem3a  6476  tfr0dm  6488  tfrlemisucaccv  6491  tfrlemiex  6497  tfrlemi1  6498  tfrlemi14d  6499  tfrexlem  6500  tfr1onlem3ag  6503  tfr1onlemsucaccv  6507  tfr1onlemex  6513  tfr1onlemaccex  6514  tfr1onlemres  6515  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  tfrcllemex  6526  tfrcllemaccex  6527  tfrcllemres  6528  tfrcldm  6529  frec0g  6563  frecabcl  6565  freccllem  6568  frecfcllem  6570  frecsuclem  6572  frecsuc  6573  nnacan  6680  nnmcan  6687  nnaordex  6696  ertr  6717  brecop  6794  eroveu  6795  ecopovtrn  6801  ecopovtrng  6804  th3qlem1  6806  th3qlem2  6807  th3q  6809  elpm2r  6835  mapsncnv  6864  elixp2  6871  ixpeq1  6878  elixpsn  6904  ixpsnf1o  6905  mapsnen  6986  map1  6987  xpsnen  7005  endisj  7008  pw2f1odclem  7020  xpf1o  7030  phplem3g  7042  ssfiexmid  7063  ssfiexmidt  7065  domfiexmid  7067  findcard2s  7079  isinfinf  7086  ac6sfi  7087  fiintim  7123  fisseneq  7127  opabfi  7132  f1dmvrnfibi  7143  sbthlem2  7157  isbth  7166  supeq1  7185  supeq3  7189  supeq123d  7190  supmoti  7192  eqsupti  7195  supsnti  7204  isotilem  7205  isoti  7206  supisolem  7207  supisoex  7208  cnvinfex  7217  cnvti  7218  eqinfti  7219  infvalti  7221  updjud  7281  ctssexmid  7349  omniwomnimkv  7366  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  acneq  7417  acfun  7422  tapeq1  7471  tapeq2  7472  exmidapne  7479  ccfunen  7483  cc2lem  7485  cc3  7487  ltsopi  7540  recexnq  7610  recmulnqg  7611  ltsonq  7618  lt2addnq  7624  lt2mulnq  7625  ltbtwnnqq  7635  prarloclemarch2  7639  enq0sym  7652  enq0ref  7653  enq0tr  7654  enq0breq  7656  addnq0mo  7667  mulnq0mo  7668  addnnnq0  7669  mulnnnq0  7670  nqnq0a  7674  nqnq0m  7675  elinp  7694  prcdnql  7704  prcunqu  7705  prltlu  7707  prdisj  7712  prarloclemlo  7714  prarloclem3  7717  prarloclem5  7720  ltdfpr  7726  genprndl  7741  genprndu  7742  genpdisj  7743  appdivnq  7783  ltpopr  7815  ltexprlemdisj  7826  ltexprlemloc  7827  ltexprlemrl  7830  ltexprlemru  7832  ltexpri  7833  recexprlemm  7844  recexprlemdisj  7850  recexprlemloc  7851  recexprlem1ssl  7853  recexprlem1ssu  7854  recexpr  7858  aptiprleml  7859  archpr  7863  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  cauappcvgprlem1  7879  cauappcvgprlemlim  7881  cauappcvgpr  7882  caucvgprlemnkj  7886  caucvgprlemnbj  7887  caucvgprlemcl  7896  caucvgpr  7902  caucvgprprlemcbv  7907  caucvgprprlemval  7908  caucvgprprlemopu  7919  caucvgprpr  7932  suplocexpr  7945  addsrmo  7963  mulsrmo  7964  addsrpr  7965  mulsrpr  7966  lttrsr  7982  recexgt0sr  7993  caucvgsrlemcau  8013  caucvgsrlemgt1  8015  caucvgsrlemoffcau  8018  caucvgsrlemoffres  8020  caucvgsr  8022  suplocsrlem  8028  ltresr  8059  pitonn  8068  peano1nnnn  8072  peano2nnnn  8073  axprecex  8100  axcnre  8101  axpre-lttrn  8104  peano5nnnn  8112  axcaucvglemcau  8118  axcaucvglemres  8119  axpre-suploclemres  8121  axpre-suploc  8122  axlttrn  8248  axsuploc  8252  letri3  8260  letr  8262  le2add  8624  lt2add  8625  ltleadd  8626  lt2sub  8640  le2sub  8641  apreap  8767  apreim  8783  apti  8802  msq11  9082  dfinfre  9136  sup3exmid  9137  cju  9141  peano5nni  9146  1nn  9154  peano2nn  9155  nn2ge  9176  nominpos  9382  elz2  9551  dfuzi  9590  uzind  9591  supinfneg  9829  infsupneg  9830  elpqb  9884  xrletri3  10039  xrletr  10043  z2ge  10061  elixx1  10132  elioo2  10156  iooshf  10187  iooneg  10223  iccneg  10224  icoshft  10225  elfz1  10248  fzdifsuc  10316  fzrev  10319  1fv  10374  zsupcllemstep  10490  infssuzex  10494  nninfdcex  10498  zsupssdc  10499  exbtwnzlemstep  10508  exbtwnzlemshrink  10509  exbtwnzlemex  10510  exbtwnz  10511  rebtwn2zlemstep  10513  rebtwn2zlemshrink  10514  rebtwn2z  10515  qbtwnre  10517  qbtwnxr  10518  flval  10533  flqlelt  10537  flqbi  10551  flqbi2  10552  modqid2  10614  q2submod  10648  seqf1og  10784  nnesq  10922  hashunlem  11068  zfz1isolem1  11105  zfz1iso  11106  seq3coll  11107  fundm2domnop0  11113  pfxsuffeqwrdeq  11283  swrdpfx  11292  wrd2ind  11308  swrdccatin2  11314  swrdccatin2d  11329  pfxccatin12d  11330  reuccatpfxs1lem  11331  reuccatpfxs1  11332  shftlem  11394  shftfibg  11398  shftfib  11401  shftfn  11402  2shfti  11409  cjval  11423  cjth  11424  remim  11438  caucvgrelemcau  11558  caucvgre  11559  cvg1nlemcau  11562  cvg1nlemres  11563  rexanuz2  11569  recvguniq  11573  resqrexlemgt0  11598  resqrexlemoverl  11599  resqrexlemglsq  11600  resqrexlemsqa  11602  resqrexlemex  11603  rsqrmo  11605  resqrtcl  11607  rersqrtthlem  11608  absdiflt  11670  absdifle  11671  cau3lem  11692  icodiamlt  11758  maxleast  11791  negfi  11806  minmax  11808  lemininf  11812  ltmininf  11813  xrmaxlesup  11837  xrminmax  11843  xrltmininf  11848  xrlemininf  11849  iooinsup  11855  clim  11859  clim2  11861  climshftlemg  11880  addcn2  11888  climcau  11925  summodc  11962  fsum3  11966  fsum2dlemstep  12013  fisumcom2  12017  fsum00  12041  ntrivcvgap0  12128  prodeq1f  12131  prodeq2w  12135  prodeq2  12136  prodmodc  12157  zproddc  12158  fprodseq  12162  fprodntrivap  12163  fprod2dlemstep  12201  fprodcom2fi  12205  sin01bnd  12336  cos01bnd  12337  divalgmod  12506  ndvdssub  12509  gcdsupex  12546  gcdsupcl  12547  gcddvds  12552  dvdslegcd  12553  bezoutlemmain  12587  bezoutlemex  12590  bezoutlemzz  12591  bezoutlemeu  12596  bezoutlemle  12597  bezoutlemsup  12598  dfgcd3  12599  dfgcd2  12603  gcddiv  12608  lcmval  12653  lcmcllem  12657  dvdslcm  12659  lcmledvds  12660  lcmgcdlem  12667  lcmdvds  12669  coprmgcdb  12678  ncoprmgcdne1b  12679  coprmdvds1  12681  qredeu  12687  divgcdcoprm0  12691  divgcdcoprmex  12692  isprm3  12708  pw2dvdslemn  12755  pw2dvdseu  12758  oddpwdclemxy  12759  qnumdencl  12777  qnumdenbi  12782  crth  12814  reumodprminv  12844  pythagtriplem19  12873  pceu  12886  pczpre  12888  pcdiv  12893  pc11  12922  dvdsprmpweqle  12928  prmpwdvds  12946  pockthi  12949  infpnlem2  12951  elgz  12962  4sqlem12  12993  ennnfonelemim  13063  exmidunben  13065  ctinfom  13067  ctiunctlemu1st  13073  ctiunctlemu2nd  13074  ctiunctlemudc  13076  ctiunctlemfo  13078  infpn2  13095  ptex  13365  prdsval  13374  f1ocpbllem  13411  ercpbl  13432  erlecpbl  13433  grpidvalg  13474  grpidpropdg  13475  mgmlrid  13480  igsumvalx  13490  gsumfzval  13492  gsumress  13496  gsumval2  13498  issgrpd  13513  sgrppropd  13514  ismnddef  13519  sgrpidmndm  13521  ismndd  13538  mndpropd  13541  mndinvmod  13546  mnd1  13556  ismhm  13562  mhmex  13563  mhmpropd  13567  issubm  13573  insubm  13586  grppropd  13618  dfgrp2  13628  isgrpid2  13641  isgrpinv  13655  grplrinv  13658  grpidinv2  13659  grpidinv  13660  dfgrp3mlem  13699  grplactcnv  13703  releqgg  13825  eqgex  13826  eqgfval  13827  eqgval  13828  isghm  13848  ghmrn  13862  resghm  13865  ghmpropd  13888  cmnpropd  13900  ablpropd  13901  imasabl  13941  isrng  13966  rngdi  13972  rngdir  13973  rngpropd  13987  dfur2g  13994  issrg  13997  srgideu  14004  srgidmlem  14010  issrgid  14013  srg1zr  14019  isring  14032  ringideu  14049  ringidmlem  14054  isringid  14057  ringid  14058  ringpropd  14070  ring1  14091  oppr0g  14113  oppr1g  14114  dvdsrvald  14126  dvdsrd  14127  dvdsrtr  14134  unitgrp  14149  dvdsrpropdg  14180  unitpropdg  14181  rhmopp  14209  opprnzrbg  14218  opprsubrngg  14244  issubrg  14254  subrg1  14264  subrgugrp  14273  resrhm2b  14282  subrgpropd  14286  rhmpropd  14287  opprdomnbg  14307  aprval  14315  aprap  14319  islmod  14324  lmodlema  14325  islmodd  14326  lmodfopnelem2  14358  lmodprop2d  14381  islssm  14390  islssmg  14391  rnglidlrng  14531  isridl  14537  df2idl2rng  14541  quscrng  14566  istopg  14742  fiinbas  14792  eltg2  14796  topbas  14810  neiint  14888  neipsm  14897  opnneissb  14898  opnssneib  14899  innei  14906  restbasg  14911  iscnp4  14961  cnpnei  14962  cnconst2  14976  cnptopresti  14981  cnptoprest  14982  cnpdis  14985  lmss  14989  lmres  14991  txbas  15001  eltx  15002  neitx  15011  txcnp  15014  txcnmpt  15016  uptx  15017  txdis  15020  txdis1cn  15021  txlm  15022  txhmeo  15062  ispsmet  15066  ismet  15087  isxmet  15088  bldisj  15144  blininf  15167  blssexps  15172  blssex  15173  ssblex  15174  xmspropd  15220  mspropd  15221  neibl  15234  metequiv  15238  bdmopn  15247  metrest  15249  xmetxp  15250  xmetxpbl  15251  xmettx  15253  metcnp3  15254  tgioo  15297  tgqioo  15298  addcncntoplem  15304  mpomulcn  15309  mulcncflem  15350  dedekindeu  15366  dedekindicclemicc  15375  limccl  15402  ellimc3apf  15403  limcimolemlt  15407  limccoap  15421  elply2  15478  sin0pilem2  15525  sincosq1sgn  15569  sincosq2sgn  15570  sincosq3sgn  15571  sincosq4sgn  15572  perfect  15744  lgsval  15752  lgsdir2lem5  15780  lgsne0  15786  lgsquadlem1  15825  lgsquadlem2  15826  lgsquadlem3  15827  lgsquad  15828  2lgslem3  15849  2sqlem8a  15870  2sqlem8  15871  2sqlem9  15872  gropd  15917  grstructd2dom  15918  incistruhgr  15960  uhgr2edg  16076  vtxd0nedgbfi  16169  wlkeq  16224  istrl  16255  clwwlkn2  16291  eupthsg  16315  iseupth  16317  eupth2lem1  16328  depind  16379  bj-sseq  16439  bj-charfunbi  16457  bj-nalset  16541  bj-indeq  16575  bj-2inf  16584  strcoll2  16629  strcollnft  16630  strcollnfALT  16632  sscoll2  16634  subctctexmid  16652  domomsubct  16653  exmidsbthrlem  16677  sbthom  16681  qdencn  16682  qdiff  16704  ltlenmkv  16726  gfsumval  16732