Theorem anbi12d 477

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 469	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜃)))
3		anbi12d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	3	anbi2d 468	. 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜃) ↔ (𝜒 ∧ 𝜏)))
5	2, 4	bitrd 188	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜏)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm4.38  613  pm5.17dc  916  orbididc  966  ifpbi123d  1005  3anbi123d  1353  xorbi2d  1429  xorbi1d  1430  drsb1  1852  mopick  2165  clelab  2366  cbvrmow  2735  cbvrexfw  2776  cbvrexf  2778  cbvreu  2784  cbvrexvw  2791  cbvreuvw  2792  cbvrexdva2  2794  cbvrab  2819  gencbvex  2869  rspce  2924  eqvincf  2951  ceqsrexv  2956  elrabf  2980  rexab2  2992  reu2  3014  reu6  3015  rmo4  3019  reu8  3022  reuind  3031  sbcan  3094  sbcang  3095  reu8nf  3133  sbcabel  3134  rmob  3145  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  difjust  3221  injust  3225  eldif  3229  ssconb  3362  elin  3412  opeq1  3904  opeq2  3905  2ralunsn  3924  elunii  3940  csbunig  3943  eluniab  3947  cbvopab  4203  cbvopab1  4205  cbvopab2  4206  cbvopab1s  4207  cbvopab2v  4209  cbvmptf  4227  cbvmpt  4228  trel  4238  nalset  4265  elssabg  4286  mss  4368  exss  4369  opelopab2a  4409  poeq1  4446  pocl  4450  soeq1  4462  weeq1  4503  weeq2  4504  ordeq  4519  zfun  4581  snnex  4596  reusv3  4608  ontr2exmid  4674  regexmid  4684  onintexmid  4722  reg3exmid  4729  peano5  4747  limom  4763  nnregexmid  4770  vtoclr  4825  opeliunxp  4832  poinxp  4846  opbrop  4856  csbxpg  4858  opeliunxp2  4922  relop  4932  brcogw  4951  elrnmpt1  5035  elsnres  5102  dfres2  5118  inimasn  5208  xpcanm  5230  xpcan2m  5231  elxp4  5278  elxp5  5279  cnvsom  5334  sbcfung  5404  funopg  5414  fununi  5452  funcnvuni  5453  fneq1  5472  2elresin  5497  feq1  5519  sbcfng  5534  sbcfg  5535  f1eq1  5596  foeq1  5614  f1oeq1  5630  f1oeq2  5631  f1oeq3  5632  ffoss  5675  brprcneu  5691  fv3  5721  tz6.12f  5727  ssimaex  5767  fvopab3g  5781  fvopab3ig  5782  fvopab6  5808  fmptco  5877  fsn2g  5886  funopsn  5894  funopdmsn  5898  elunirn  5975  f1imaeq  5984  foeqcnvco  5999  fliftfun  6005  fliftval  6009  isoeq1  6010  isoeq4  6013  isoini  6027  isopolem  6031  f1oiso2  6036  riotabidv  6043  cbvriotavw  6052  cbvriota  6053  acexmid  6087  ovanraleqv  6112  cbvoprab1  6163  cbvoprab2  6164  cbvoprab12  6165  cbvmpox  6169  ov  6211  ovig  6213  ovg  6231  caovimo  6286  caoftrn  6339  opabex3d  6354  opabex3  6355  uchoice  6375  elxp6  6407  unielxp  6412  dfoprab4  6430  dfoprab4f  6431  fmpox  6440  xporderlem  6471  poxp  6472  cnvoprab  6474  f1od2  6475  opeliunxp2f  6514  rbropapd  6518  dftpos4  6539  tpostpos  6540  smoiso  6578  tfrlem3ag  6585  tfrlem3a  6586  tfr0dm  6598  tfrlemisucaccv  6601  tfrlemiex  6607  tfrlemi1  6608  tfrlemi14d  6609  tfrexlem  6610  tfr1onlem3ag  6613  tfr1onlemsucaccv  6617  tfr1onlemex  6623  tfr1onlemaccex  6624  tfr1onlemres  6625  tfrcllemsucaccv  6630  tfrcllembxssdm  6632  tfrcllemex  6636  tfrcllemaccex  6637  tfrcllemres  6638  tfrcldm  6639  frec0g  6673  frecabcl  6675  freccllem  6678  frecfcllem  6680  frecsuclem  6682  frecsuc  6683  nnacan  6790  nnmcan  6797  nnaordex  6806  ertr  6827  brecop  6904  eroveu  6905  ecopovtrn  6911  ecopovtrng  6914  th3qlem1  6916  th3qlem2  6917  th3q  6919  elpm2r  6945  mapsncnv  6983  elixp2  6990  ixpeq1  6997  elixpsn  7023  ixpsnf1o  7024  mapsnend  7105  mapsnen  7106  map1  7107  xpsnen  7125  endisj  7128  pw2f1odclem  7140  xpf1o  7150  mapunen  7157  phplem3g  7163  ssfiexmid  7184  ssfiexmidt  7186  domfiexmid  7188  findcard2s  7200  isinfinf  7207  ac6sfi  7208  fiintim  7244  fisseneq  7248  opabfi  7253  f1dmvrnfibi  7264  sbthlem2  7282  isbth  7291  isfsuppfi  7296  supeq1  7332  supeq3  7336  supeq123d  7337  supmoti  7339  eqsupti  7342  supsnti  7351  isotilem  7352  isoti  7353  supisolem  7354  supisoex  7355  cnvinfex  7364  cnvti  7365  eqinfti  7366  infvalti  7368  updjud  7428  ctssexmid  7496  omniwomnimkv  7513  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  acneq  7564  acfun  7569  papeq1  7615  papeq2  7616  tapeq1  7624  tapeq2  7625  exmidapne  7632  ccfunen  7636  cc2lem  7638  cc3  7640  ltsopi  7693  recexnq  7763  recmulnqg  7764  ltsonq  7771  lt2addnq  7777  lt2mulnq  7778  ltbtwnnqq  7788  prarloclemarch2  7792  enq0sym  7805  enq0ref  7806  enq0tr  7807  enq0breq  7809  addnq0mo  7820  mulnq0mo  7821  addnnnq0  7822  mulnnnq0  7823  nqnq0a  7827  nqnq0m  7828  elinp  7847  prcdnql  7857  prcunqu  7858  prltlu  7860  prdisj  7865  prarloclemlo  7867  prarloclem3  7870  prarloclem5  7873  ltdfpr  7879  genprndl  7894  genprndu  7895  genpdisj  7896  appdivnq  7936  ltpopr  7968  ltexprlemdisj  7979  ltexprlemloc  7980  ltexprlemrl  7983  ltexprlemru  7985  ltexpri  7986  recexprlemm  7997  recexprlemdisj  8003  recexprlemloc  8004  recexprlem1ssl  8006  recexprlem1ssu  8007  recexpr  8011  aptiprleml  8012  archpr  8016  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  cauappcvgprlem1  8032  cauappcvgprlemlim  8034  cauappcvgpr  8035  caucvgprlemnkj  8039  caucvgprlemnbj  8040  caucvgprlemcl  8049  caucvgpr  8055  caucvgprprlemcbv  8060  caucvgprprlemval  8061  caucvgprprlemopu  8072  caucvgprpr  8085  suplocexpr  8098  addsrmo  8116  mulsrmo  8117  addsrpr  8118  mulsrpr  8119  lttrsr  8135  recexgt0sr  8146  caucvgsrlemcau  8166  caucvgsrlemgt1  8168  caucvgsrlemoffcau  8171  caucvgsrlemoffres  8173  caucvgsr  8175  suplocsrlem  8181  ltresr  8212  pitonn  8221  peano1nnnn  8225  peano2nnnn  8226  axprecex  8253  axcnre  8254  axpre-lttrn  8257  peano5nnnn  8265  axcaucvglemcau  8271  axcaucvglemres  8272  axpre-suploclemres  8274  axpre-suploc  8275  axlttrn  8400  axsuploc  8404  letri3  8412  letr  8414  le2add  8779  lt2add  8780  ltleadd  8781  lt2sub  8795  le2sub  8796  apreap  8923  apreim  8939  apti  8958  msq11  9240  dfinfre  9294  sup3exmid  9295  cju  9299  peano5nni  9316  1nn  9324  peano2nn  9325  nn2ge  9346  nominpos  9554  elz2  9725  dfuzi  9766  uzind  9767  supinfneg  10010  infsupneg  10011  elpqb  10066  xrletri3  10222  xrletr  10226  z2ge  10244  elixx1  10315  elioo2  10339  iooshf  10370  iooneg  10406  iccneg  10407  icoshft  10408  elfz1  10432  fzdifsuc  10504  fzrev  10507  1fv  10562  zsupcllemstep  10678  infssuzex  10682  nninfdcex  10688  zsupssdc  10689  exbtwnzlemstep  10698  exbtwnzlemshrink  10699  exbtwnzlemex  10700  exbtwnz  10701  rebtwn2zlemstep  10703  rebtwn2zlemshrink  10704  rebtwn2z  10705  qbtwnre  10707  qbtwnxr  10708  flval  10723  flqlelt  10728  flaplelt  10729  flqbi  10745  flqbi2  10746  modqid2  10808  q2submod  10842  seqf1og  10978  nnesq  11117  hashunlem  11265  hashfibclem  11303  hashf1lem1  11306  hashf1lem2  11307  zfz1isolem1  11313  zfz1iso  11314  seq3coll  11315  fundm2domnop0  11321  pfxsuffeqwrdeq  11491  swrdpfx  11500  wrd2ind  11516  swrdccatin2  11522  swrdccatin2d  11537  pfxccatin12d  11538  reuccatpfxs1lem  11539  reuccatpfxs1  11540  shftlem  11602  shftfibg  11606  shftfib  11609  shftfn  11610  2shfti  11617  cjval  11631  cjth  11632  remim  11646  caucvgrelemcau  11767  caucvgre  11768  cvg1nlemcau  11771  cvg1nlemres  11772  rexanuz2  11778  recvguniq  11782  resqrexlemgt0  11807  resqrexlemoverl  11808  resqrexlemglsq  11809  resqrexlemsqa  11811  resqrexlemex  11812  rsqrmo  11814  resqrtcl  11816  rersqrtthlem  11817  absdiflt  11880  absdifle  11881  cau3lem  11902  icodiamlt  11968  maxleast  12001  negfi  12016  minmax  12019  lemininf  12023  ltmininf  12024  xrmaxlesup  12049  xrminmax  12055  xrltmininf  12060  xrlemininf  12061  iooinsup  12067  clim  12071  clim2  12073  climshftlemg  12092  addcn2  12100  climcau  12137  summodc  12174  fsum3  12178  fsum2dlemstep  12225  fisumcom2  12229  fsum00  12253  ntrivcvgap0  12340  prodeq1f  12343  prodeq2w  12347  prodeq2  12348  prodmodc  12369  zproddc  12370  fprodseq  12374  fprodntrivap  12375  fprod2dlemstep  12413  fprodcom2fi  12417  sin01bnd  12548  cos01bnd  12549  divalgmod  12718  ndvdssub  12721  gcdsupex  12758  gcdsupcl  12759  gcddvds  12764  dvdslegcd  12765  bezoutlemmain  12799  bezoutlemex  12802  bezoutlemzz  12803  bezoutlemeu  12808  bezoutlemle  12809  bezoutlemsup  12810  dfgcd3  12811  dfgcd2  12815  gcddiv  12820  lcmval  12865  lcmcllem  12869  dvdslcm  12871  lcmledvds  12872  lcmgcdlem  12879  lcmdvds  12881  coprmgcdb  12890  ncoprmgcdne1b  12891  coprmdvds1  12893  qredeu  12899  divgcdcoprm0  12903  divgcdcoprmex  12904  isprm3  12920  pwbdvdslemn  12968  pwbdvdseu  12971  nnmaxpwlemxy  12972  qnumdencl  12991  qnumdenbi  12996  crth  13030  reumodprminv  13060  pythagtriplem19  13089  pceu  13102  pczpre  13104  pcdiv  13109  pc11  13138  dvdsprmpweqle  13144  prmpwdvds  13162  pockthi  13165  infpnlem2  13167  elgz  13178  4sqlem12  13209  ennnfonelemim  13372  exmidunben  13374  ctinfom  13376  ctiunctlemu1st  13382  ctiunctlemu2nd  13383  ctiunctlemudc  13385  ctiunctlemfo  13387  infpn2  13404  ptex  13676  f1ocpbllem  13689  ercpbl  13710  erlecpbl  13711  grpidvalg  13751  grpidpropdg  13752  mgmlrid  13757  gzsumvalx  13767  gzsumfzval  13769  gzsumress  13770  gzsumval2  13772  issgrpd  13785  sgrppropd  13786  ismnddef  13789  sgrpidmndm  13791  ismndd  13808  mndpropd  13811  mndinvmod  13816  mnd1  13820  ismhm  13826  mhmex  13827  mhmpropd  13831  issubm  13837  insubm  13850  grppropd  13880  dfgrp2  13890  isgrpid2  13903  isgrpinv  13917  grplrinv  13920  grpidinv2  13921  grpidinv  13922  dfgrp3mlem  13961  grplactcnv  13965  releqgg  14081  eqgex  14082  eqgfval  14083  eqgval  14084  isghm  14104  ghmrn  14118  resghm  14121  ghmpropd  14144  resscntz  14165  cmnpropd  14187  ablpropd  14188  imasabl  14229  gsumvalfi  14241  prdsval  14279  isrng  14339  rngdi  14345  rngdir  14346  rngpropd  14360  rng1zrlem  14364  dfur2g  14372  issrg  14375  srgideu  14382  srgidmlem  14388  issrgid  14391  isring  14410  ringideu  14427  ringidmlem  14433  isringid  14436  ringid  14437  ringpropd  14449  ring1  14470  oppr0g  14495  oppr1g  14496  dvdsrvald  14508  dvdsrd  14509  dvdsrtr  14516  unitgrp  14531  dvdsrpropdg  14562  unitpropdg  14563  rhmopp  14591  opprnzrbg  14600  opprlring  14612  opprsubrngg  14627  issubrg  14637  subrg1  14647  subrgugrp  14656  resrhm2b  14665  subrgpropd  14669  rhmpropd  14670  opprdomnbg  14691  aprval  14699  aprap  14706  aprprop  14709  opprdrng  14728  islmod  14735  lmodlema  14736  islmodd  14737  lmodfopnelem2  14770  lmodprop2d  14793  islssm  14802  islssmg  14803  rnglidlrng  14943  isridl  14949  df2idl2rng  14953  quscrng  14978  isassa  15110  assalem  15111  isassad  15119  assapropd  15122  psrbagmax  15183  istopg  15242  fiinbas  15292  eltg2  15296  topbas  15310  neiint  15388  neipsm  15397  opnneissb  15398  opnssneib  15399  innei  15406  restbasg  15411  iscnp4  15461  cnpnei  15462  cnconst2  15476  cnptopresti  15481  cnptoprest  15482  cnpdis  15485  lmss  15489  lmres  15491  txbas  15501  eltx  15502  neitx  15511  txcnp  15514  txcnmpt  15516  uptx  15517  txdis  15520  txdis1cn  15521  txlm  15522  txhmeo  15562  ispsmet  15566  ismet  15587  isxmet  15588  bldisj  15644  blininf  15667  blssexps  15672  blssex  15673  ssblex  15674  xmspropd  15720  mspropd  15721  neibl  15734  metequiv  15738  bdmopn  15747  metrest  15749  xmetxp  15750  xmetxpbl  15751  xmettx  15753  metcnp3  15754  tgioo  15797  tgqioo  15798  addcncntoplem  15804  mpomulcn  15809  mulcncflem  15850  dedekindeu  15866  dedekindicclemicc  15875  limccl  15902  ellimc3apf  15903  limcimolemlt  15907  limccoap  15921  elply2  15978  sin0pilem2  16026  sincosq1sgn  16070  sincosq2sgn  16071  sincosq3sgn  16072  sincosq4sgn  16073  zprmlogbaplem3  16234  zprmlogbap  16235  pellexlem3  16248  perfect  16318  prmefexple  16325  bpos1lem  16326  bposlem1  16328  bposlem9  16336  lgsval  16345  lgsdir2lem5  16373  lgsne0  16379  lgsquadlem1  16418  lgsquadlem2  16419  lgsquadlem3  16420  lgsquad  16421  2lgslem3  16442  2sqlem8a  16463  2sqlem8  16464  2sqlem9  16465  gropd  16510  grstructd2dom  16511  incistruhgr  16553  uhgr2edg  16669  vtxd0nedgbfi  16762  wlkeq  16817  istrl  16848  clwwlkn2  16884  eupthsg  16908  iseupth  16910  eupth2lem1  16921  depind  16972  bj-sseq  17042  bj-charfunbi  17059  bj-nalset  17143  bj-indeq  17177  bj-2inf  17186  strcoll2  17231  strcollnft  17232  strcollnfALT  17234  sscoll2  17236  subctctexmid  17252  domomsubct  17253  exmidsbthrlem  17290  sbthom  17294  qdencn  17295  qdiff  17322  ltlenmkv  17344  alsbid  17367