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  4202  cbvopab1  4204  cbvopab2  4205  cbvopab1s  4206  cbvopab2v  4208  cbvmptf  4225  cbvmpt  4226  trel  4236  nalset  4263  elssabg  4284  mss  4366  exss  4367  opelopab2a  4407  poeq1  4444  pocl  4448  soeq1  4460  weeq1  4501  weeq2  4502  ordeq  4517  zfun  4579  snnex  4594  reusv3  4606  ontr2exmid  4672  regexmid  4682  onintexmid  4720  reg3exmid  4727  peano5  4745  limom  4761  nnregexmid  4768  vtoclr  4823  opeliunxp  4830  poinxp  4844  opbrop  4854  csbxpg  4856  opeliunxp2  4920  relop  4930  brcogw  4949  elrnmpt1  5033  elsnres  5100  dfres2  5115  inimasn  5205  xpcanm  5227  xpcan2m  5228  elxp4  5275  elxp5  5276  cnvsom  5331  sbcfung  5401  funopg  5411  fununi  5449  funcnvuni  5450  fneq1  5469  2elresin  5494  feq1  5516  sbcfng  5531  sbcfg  5532  f1eq1  5593  foeq1  5611  f1oeq1  5627  f1oeq2  5628  f1oeq3  5629  ffoss  5672  brprcneu  5688  fv3  5718  tz6.12f  5724  ssimaex  5764  fvopab3g  5778  fvopab3ig  5779  fvopab6  5805  fmptco  5874  fsn2g  5883  funopsn  5891  funopdmsn  5895  elunirn  5972  f1imaeq  5981  foeqcnvco  5996  fliftfun  6002  fliftval  6006  isoeq1  6007  isoeq4  6010  isoini  6024  isopolem  6028  f1oiso2  6033  riotabidv  6040  cbvriotavw  6049  cbvriota  6050  acexmid  6084  ovanraleqv  6109  cbvoprab1  6160  cbvoprab2  6161  cbvoprab12  6162  cbvmpox  6166  ov  6208  ovig  6210  ovg  6228  caovimo  6283  caoftrn  6335  opabex3d  6350  opabex3  6351  uchoice  6371  elxp6  6403  unielxp  6408  dfoprab4  6426  dfoprab4f  6427  fmpox  6436  xporderlem  6467  poxp  6468  cnvoprab  6470  f1od2  6471  opeliunxp2f  6509  rbropapd  6513  dftpos4  6534  tpostpos  6535  smoiso  6573  tfrlem3ag  6580  tfrlem3a  6581  tfr0dm  6593  tfrlemisucaccv  6596  tfrlemiex  6602  tfrlemi1  6603  tfrlemi14d  6604  tfrexlem  6605  tfr1onlem3ag  6608  tfr1onlemsucaccv  6612  tfr1onlemex  6618  tfr1onlemaccex  6619  tfr1onlemres  6620  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllemex  6631  tfrcllemaccex  6632  tfrcllemres  6633  tfrcldm  6634  frec0g  6668  frecabcl  6670  freccllem  6673  frecfcllem  6675  frecsuclem  6677  frecsuc  6678  nnacan  6785  nnmcan  6792  nnaordex  6801  ertr  6822  brecop  6899  eroveu  6900  ecopovtrn  6906  ecopovtrng  6909  th3qlem1  6911  th3qlem2  6912  th3q  6914  elpm2r  6940  mapsncnv  6977  elixp2  6984  ixpeq1  6991  elixpsn  7017  ixpsnf1o  7018  mapsnend  7099  mapsnen  7100  map1  7101  xpsnen  7119  endisj  7122  pw2f1odclem  7134  xpf1o  7144  mapunen  7151  phplem3g  7157  ssfiexmid  7178  ssfiexmidt  7180  domfiexmid  7182  findcard2s  7194  isinfinf  7201  ac6sfi  7202  fiintim  7238  fisseneq  7242  opabfi  7247  f1dmvrnfibi  7258  sbthlem2  7275  isbth  7284  isfsupp  7289  supeq1  7327  supeq3  7331  supeq123d  7332  supmoti  7334  eqsupti  7337  supsnti  7346  isotilem  7347  isoti  7348  supisolem  7349  supisoex  7350  cnvinfex  7359  cnvti  7360  eqinfti  7361  infvalti  7363  updjud  7423  ctssexmid  7491  omniwomnimkv  7508  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  acneq  7559  acfun  7564  papeq1  7610  papeq2  7611  tapeq1  7619  tapeq2  7620  exmidapne  7627  ccfunen  7631  cc2lem  7633  cc3  7635  ltsopi  7688  recexnq  7758  recmulnqg  7759  ltsonq  7766  lt2addnq  7772  lt2mulnq  7773  ltbtwnnqq  7783  prarloclemarch2  7787  enq0sym  7800  enq0ref  7801  enq0tr  7802  enq0breq  7804  addnq0mo  7815  mulnq0mo  7816  addnnnq0  7817  mulnnnq0  7818  nqnq0a  7822  nqnq0m  7823  elinp  7842  prcdnql  7852  prcunqu  7853  prltlu  7855  prdisj  7860  prarloclemlo  7862  prarloclem3  7865  prarloclem5  7868  ltdfpr  7874  genprndl  7889  genprndu  7890  genpdisj  7891  appdivnq  7931  ltpopr  7963  ltexprlemdisj  7974  ltexprlemloc  7975  ltexprlemrl  7978  ltexprlemru  7980  ltexpri  7981  recexprlemm  7992  recexprlemdisj  7998  recexprlemloc  7999  recexprlem1ssl  8001  recexprlem1ssu  8002  recexpr  8006  aptiprleml  8007  archpr  8011  cauappcvgprlemladdru  8024  cauappcvgprlemladdrl  8025  cauappcvgprlem1  8027  cauappcvgprlemlim  8029  cauappcvgpr  8030  caucvgprlemnkj  8034  caucvgprlemnbj  8035  caucvgprlemcl  8044  caucvgpr  8050  caucvgprprlemcbv  8055  caucvgprprlemval  8056  caucvgprprlemopu  8067  caucvgprpr  8080  suplocexpr  8093  addsrmo  8111  mulsrmo  8112  addsrpr  8113  mulsrpr  8114  lttrsr  8130  recexgt0sr  8141  caucvgsrlemcau  8161  caucvgsrlemgt1  8163  caucvgsrlemoffcau  8166  caucvgsrlemoffres  8168  caucvgsr  8170  suplocsrlem  8176  ltresr  8207  pitonn  8216  peano1nnnn  8220  peano2nnnn  8221  axprecex  8248  axcnre  8249  axpre-lttrn  8252  peano5nnnn  8260  axcaucvglemcau  8266  axcaucvglemres  8267  axpre-suploclemres  8269  axpre-suploc  8270  axlttrn  8395  axsuploc  8399  letri3  8407  letr  8409  le2add  8774  lt2add  8775  ltleadd  8776  lt2sub  8790  le2sub  8791  apreap  8918  apreim  8934  apti  8953  msq11  9235  dfinfre  9289  sup3exmid  9290  cju  9294  peano5nni  9310  1nn  9318  peano2nn  9319  nn2ge  9340  nominpos  9548  elz2  9721  dfuzi  9761  uzind  9762  supinfneg  10005  infsupneg  10006  elpqb  10061  xrletri3  10217  xrletr  10221  z2ge  10239  elixx1  10310  elioo2  10334  iooshf  10365  iooneg  10401  iccneg  10402  icoshft  10403  elfz1  10427  fzdifsuc  10499  fzrev  10502  1fv  10557  zsupcllemstep  10673  infssuzex  10677  nninfdcex  10683  zsupssdc  10684  exbtwnzlemstep  10693  exbtwnzlemshrink  10694  exbtwnzlemex  10695  exbtwnz  10696  rebtwn2zlemstep  10698  rebtwn2zlemshrink  10699  rebtwn2z  10700  qbtwnre  10702  qbtwnxr  10703  flval  10718  flqlelt  10723  flaplelt  10724  flqbi  10740  flqbi2  10741  modqid2  10803  q2submod  10837  seqf1og  10973  nnesq  11112  hashunlem  11260  hashfibclem  11298  hashf1lem1  11301  hashf1lem2  11302  zfz1isolem1  11308  zfz1iso  11309  seq3coll  11310  fundm2domnop0  11316  pfxsuffeqwrdeq  11486  swrdpfx  11495  wrd2ind  11511  swrdccatin2  11517  swrdccatin2d  11532  pfxccatin12d  11533  reuccatpfxs1lem  11534  reuccatpfxs1  11535  shftlem  11597  shftfibg  11601  shftfib  11604  shftfn  11605  2shfti  11612  cjval  11626  cjth  11627  remim  11641  caucvgrelemcau  11762  caucvgre  11763  cvg1nlemcau  11766  cvg1nlemres  11767  rexanuz2  11773  recvguniq  11777  resqrexlemgt0  11802  resqrexlemoverl  11803  resqrexlemglsq  11804  resqrexlemsqa  11806  resqrexlemex  11807  rsqrmo  11809  resqrtcl  11811  rersqrtthlem  11812  absdiflt  11875  absdifle  11876  cau3lem  11897  icodiamlt  11963  maxleast  11996  negfi  12011  minmax  12014  lemininf  12018  ltmininf  12019  xrmaxlesup  12044  xrminmax  12050  xrltmininf  12055  xrlemininf  12056  iooinsup  12062  clim  12066  clim2  12068  climshftlemg  12087  addcn2  12095  climcau  12132  summodc  12169  fsum3  12173  fsum2dlemstep  12220  fisumcom2  12224  fsum00  12248  ntrivcvgap0  12335  prodeq1f  12338  prodeq2w  12342  prodeq2  12343  prodmodc  12364  zproddc  12365  fprodseq  12369  fprodntrivap  12370  fprod2dlemstep  12408  fprodcom2fi  12412  sin01bnd  12543  cos01bnd  12544  divalgmod  12713  ndvdssub  12716  gcdsupex  12753  gcdsupcl  12754  gcddvds  12759  dvdslegcd  12760  bezoutlemmain  12794  bezoutlemex  12797  bezoutlemzz  12798  bezoutlemeu  12803  bezoutlemle  12804  bezoutlemsup  12805  dfgcd3  12806  dfgcd2  12810  gcddiv  12815  lcmval  12860  lcmcllem  12864  dvdslcm  12866  lcmledvds  12867  lcmgcdlem  12874  lcmdvds  12876  coprmgcdb  12885  ncoprmgcdne1b  12886  coprmdvds1  12888  qredeu  12894  divgcdcoprm0  12898  divgcdcoprmex  12899  isprm3  12915  pwbdvdslemn  12963  pwbdvdseu  12966  nnmaxpwlemxy  12967  qnumdencl  12986  qnumdenbi  12991  crth  13025  reumodprminv  13055  pythagtriplem19  13084  pceu  13097  pczpre  13099  pcdiv  13104  pc11  13133  dvdsprmpweqle  13139  prmpwdvds  13157  pockthi  13160  infpnlem2  13162  elgz  13173  4sqlem12  13204  ennnfonelemim  13367  exmidunben  13369  ctinfom  13371  ctiunctlemu1st  13377  ctiunctlemu2nd  13378  ctiunctlemudc  13380  ctiunctlemfo  13382  infpn2  13399  ptex  13671  f1ocpbllem  13684  ercpbl  13705  erlecpbl  13706  grpidvalg  13746  grpidpropdg  13747  mgmlrid  13752  gzsumvalx  13762  gzsumfzval  13764  gzsumress  13765  gzsumval2  13767  issgrpd  13780  sgrppropd  13781  ismnddef  13784  sgrpidmndm  13786  ismndd  13803  mndpropd  13806  mndinvmod  13811  mnd1  13815  ismhm  13821  mhmex  13822  mhmpropd  13826  issubm  13832  insubm  13845  grppropd  13875  dfgrp2  13885  isgrpid2  13898  isgrpinv  13912  grplrinv  13915  grpidinv2  13916  grpidinv  13917  dfgrp3mlem  13956  grplactcnv  13960  releqgg  14076  eqgex  14077  eqgfval  14078  eqgval  14079  isghm  14099  ghmrn  14113  resghm  14116  ghmpropd  14139  resscntz  14160  cmnpropd  14182  ablpropd  14183  imasabl  14224  gsumvalfi  14236  prdsval  14257  isrng  14317  rngdi  14323  rngdir  14324  rngpropd  14338  rng1zrlem  14342  dfur2g  14350  issrg  14353  srgideu  14360  srgidmlem  14366  issrgid  14369  isring  14388  ringideu  14405  ringidmlem  14411  isringid  14414  ringid  14415  ringpropd  14427  ring1  14448  oppr0g  14471  oppr1g  14472  dvdsrvald  14484  dvdsrd  14485  dvdsrtr  14492  unitgrp  14507  dvdsrpropdg  14538  unitpropdg  14539  rhmopp  14567  opprnzrbg  14576  opprlring  14588  opprsubrngg  14603  issubrg  14613  subrg1  14623  subrgugrp  14632  resrhm2b  14641  subrgpropd  14645  rhmpropd  14646  opprdomnbg  14667  aprval  14675  aprap  14682  aprprop  14685  opprdrng  14704  islmod  14711  lmodlema  14712  islmodd  14713  lmodfopnelem2  14746  lmodprop2d  14769  islssm  14778  islssmg  14779  rnglidlrng  14919  isridl  14925  df2idl2rng  14929  quscrng  14954  isassa  15086  assalem  15087  isassad  15095  assapropd  15098  istopg  15191  fiinbas  15241  eltg2  15245  topbas  15259  neiint  15337  neipsm  15346  opnneissb  15347  opnssneib  15348  innei  15355  restbasg  15360  iscnp4  15410  cnpnei  15411  cnconst2  15425  cnptopresti  15430  cnptoprest  15431  cnpdis  15434  lmss  15438  lmres  15440  txbas  15450  eltx  15451  neitx  15460  txcnp  15463  txcnmpt  15465  uptx  15466  txdis  15469  txdis1cn  15470  txlm  15471  txhmeo  15511  ispsmet  15515  ismet  15536  isxmet  15537  bldisj  15593  blininf  15616  blssexps  15621  blssex  15622  ssblex  15623  xmspropd  15669  mspropd  15670  neibl  15683  metequiv  15687  bdmopn  15696  metrest  15698  xmetxp  15699  xmetxpbl  15700  xmettx  15702  metcnp3  15703  tgioo  15746  tgqioo  15747  addcncntoplem  15753  mpomulcn  15758  mulcncflem  15799  dedekindeu  15815  dedekindicclemicc  15824  limccl  15851  ellimc3apf  15852  limcimolemlt  15856  limccoap  15870  elply2  15927  sin0pilem2  15975  sincosq1sgn  16019  sincosq2sgn  16020  sincosq3sgn  16021  sincosq4sgn  16022  zprmlogbaplem3  16178  zprmlogbap  16179  pellexlem3  16192  perfect  16262  prmefexple  16269  bpos1lem  16270  bposlem1  16272  bposlem9  16280  lgsval  16289  lgsdir2lem5  16317  lgsne0  16323  lgsquadlem1  16362  lgsquadlem2  16363  lgsquadlem3  16364  lgsquad  16365  2lgslem3  16386  2sqlem8a  16407  2sqlem8  16408  2sqlem9  16409  gropd  16454  grstructd2dom  16455  incistruhgr  16497  uhgr2edg  16613  vtxd0nedgbfi  16706  wlkeq  16761  istrl  16792  clwwlkn2  16828  eupthsg  16852  iseupth  16854  eupth2lem1  16865  depind  16916  bj-sseq  16986  bj-charfunbi  17003  bj-nalset  17087  bj-indeq  17121  bj-2inf  17130  strcoll2  17175  strcollnft  17176  strcollnfALT  17178  sscoll2  17180  subctctexmid  17196  domomsubct  17197  exmidsbthrlem  17233  sbthom  17237  qdencn  17238  qdiff  17265  ltlenmkv  17287  alsbid  17310