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  607  pm5.17dc  909  orbididc  959  ifpbi123d  998  3anbi123d  1346  xorbi2d  1422  xorbi1d  1423  drsb1  1845  mopick  2156  clelab  2355  cbvrmow  2714  cbvrexfw  2755  cbvrexf  2757  cbvreu  2763  cbvrexvw  2770  cbvreuvw  2771  cbvrexdva2  2773  cbvrab  2798  gencbvex  2848  rspce  2903  eqvincf  2929  ceqsrexv  2934  elrabf  2958  rexab2  2970  reu2  2992  reu6  2993  rmo4  2997  reu8  3000  reuind  3009  sbcan  3072  sbcang  3073  reu8nf  3111  sbcabel  3112  rmob  3123  cbvrexcsf  3189  cbvreucsf  3190  cbvrabcsf  3191  difjust  3199  injust  3203  eldif  3207  ssconb  3338  elin  3388  opeq1  3860  opeq2  3861  2ralunsn  3880  elunii  3896  csbunig  3899  eluniab  3903  cbvopab  4158  cbvopab1  4160  cbvopab2  4161  cbvopab1s  4162  cbvopab2v  4164  cbvmptf  4181  cbvmpt  4182  trel  4192  nalset  4217  elssabg  4236  mss  4316  exss  4317  opelopab2a  4357  poeq1  4394  pocl  4398  soeq1  4410  weeq1  4451  weeq2  4452  ordeq  4467  zfun  4529  snnex  4543  reusv3  4555  ontr2exmid  4621  regexmid  4631  onintexmid  4669  reg3exmid  4676  peano5  4694  limom  4710  nnregexmid  4717  vtoclr  4772  opeliunxp  4779  poinxp  4793  opbrop  4803  csbxpg  4805  opeliunxp2  4868  relop  4878  brcogw  4897  elrnmpt1  4981  elsnres  5048  dfres2  5063  inimasn  5152  xpcanm  5174  xpcan2m  5175  elxp4  5222  elxp5  5223  cnvsom  5278  sbcfung  5348  funopg  5358  fununi  5395  funcnvuni  5396  fneq1  5415  2elresin  5440  feq1  5462  sbcfng  5477  sbcfg  5478  f1eq1  5534  foeq1  5552  f1oeq1  5568  f1oeq2  5569  f1oeq3  5570  ffoss  5612  brprcneu  5628  fv3  5658  tz6.12f  5664  ssimaex  5703  fvopab3g  5715  fvopab3ig  5716  fvopab6  5739  fmptco  5809  funopsn  5825  funopdmsn  5829  elunirn  5902  f1imaeq  5911  foeqcnvco  5926  fliftfun  5932  fliftval  5936  isoeq1  5937  isoeq4  5940  isoini  5954  isopolem  5958  f1oiso2  5963  riotabidv  5968  cbvriotavw  5977  cbvriota  5978  acexmid  6012  ovanraleqv  6037  cbvoprab1  6088  cbvoprab2  6089  cbvoprab12  6090  cbvmpox  6094  ov  6136  ovig  6138  ovg  6156  caovimo  6211  caoftrn  6263  opabex3d  6278  opabex3  6279  uchoice  6295  elxp6  6327  unielxp  6332  dfoprab4  6350  dfoprab4f  6351  fmpox  6360  xporderlem  6391  poxp  6392  cnvoprab  6394  f1od2  6395  opeliunxp2f  6399  rbropapd  6403  dftpos4  6424  tpostpos  6425  smoiso  6463  tfrlem3ag  6470  tfrlem3a  6471  tfr0dm  6483  tfrlemisucaccv  6486  tfrlemiex  6492  tfrlemi1  6493  tfrlemi14d  6494  tfrexlem  6495  tfr1onlem3ag  6498  tfr1onlemsucaccv  6502  tfr1onlemex  6508  tfr1onlemaccex  6509  tfr1onlemres  6510  tfrcllemsucaccv  6515  tfrcllembxssdm  6517  tfrcllemex  6521  tfrcllemaccex  6522  tfrcllemres  6523  tfrcldm  6524  frec0g  6558  frecabcl  6560  freccllem  6563  frecfcllem  6565  frecsuclem  6567  frecsuc  6568  nnacan  6675  nnmcan  6682  nnaordex  6691  ertr  6712  brecop  6789  eroveu  6790  ecopovtrn  6796  ecopovtrng  6799  th3qlem1  6801  th3qlem2  6802  th3q  6804  elpm2r  6830  mapsncnv  6859  elixp2  6866  ixpeq1  6873  elixpsn  6899  ixpsnf1o  6900  mapsnen  6981  map1  6982  xpsnen  7000  endisj  7003  pw2f1odclem  7015  xpf1o  7025  phplem3g  7037  ssfiexmid  7058  domfiexmid  7060  findcard2s  7072  isinfinf  7079  ac6sfi  7080  fiintim  7116  fisseneq  7119  opabfi  7123  f1dmvrnfibi  7134  sbthlem2  7148  isbth  7157  supeq1  7176  supeq3  7180  supeq123d  7181  supmoti  7183  eqsupti  7186  supsnti  7195  isotilem  7196  isoti  7197  supisolem  7198  supisoex  7199  cnvinfex  7208  cnvti  7209  eqinfti  7210  infvalti  7212  updjud  7272  ctssexmid  7340  omniwomnimkv  7357  exmidfodomrlemr  7403  exmidfodomrlemrALT  7404  acneq  7407  acfun  7412  tapeq1  7461  tapeq2  7462  exmidapne  7469  ccfunen  7473  cc2lem  7475  cc3  7477  ltsopi  7530  recexnq  7600  recmulnqg  7601  ltsonq  7608  lt2addnq  7614  lt2mulnq  7615  ltbtwnnqq  7625  prarloclemarch2  7629  enq0sym  7642  enq0ref  7643  enq0tr  7644  enq0breq  7646  addnq0mo  7657  mulnq0mo  7658  addnnnq0  7659  mulnnnq0  7660  nqnq0a  7664  nqnq0m  7665  elinp  7684  prcdnql  7694  prcunqu  7695  prltlu  7697  prdisj  7702  prarloclemlo  7704  prarloclem3  7707  prarloclem5  7710  ltdfpr  7716  genprndl  7731  genprndu  7732  genpdisj  7733  appdivnq  7773  ltpopr  7805  ltexprlemdisj  7816  ltexprlemloc  7817  ltexprlemrl  7820  ltexprlemru  7822  ltexpri  7823  recexprlemm  7834  recexprlemdisj  7840  recexprlemloc  7841  recexprlem1ssl  7843  recexprlem1ssu  7844  recexpr  7848  aptiprleml  7849  archpr  7853  cauappcvgprlemladdru  7866  cauappcvgprlemladdrl  7867  cauappcvgprlem1  7869  cauappcvgprlemlim  7871  cauappcvgpr  7872  caucvgprlemnkj  7876  caucvgprlemnbj  7877  caucvgprlemcl  7886  caucvgpr  7892  caucvgprprlemcbv  7897  caucvgprprlemval  7898  caucvgprprlemopu  7909  caucvgprpr  7922  suplocexpr  7935  addsrmo  7953  mulsrmo  7954  addsrpr  7955  mulsrpr  7956  lttrsr  7972  recexgt0sr  7983  caucvgsrlemcau  8003  caucvgsrlemgt1  8005  caucvgsrlemoffcau  8008  caucvgsrlemoffres  8010  caucvgsr  8012  suplocsrlem  8018  ltresr  8049  pitonn  8058  peano1nnnn  8062  peano2nnnn  8063  axprecex  8090  axcnre  8091  axpre-lttrn  8094  peano5nnnn  8102  axcaucvglemcau  8108  axcaucvglemres  8109  axpre-suploclemres  8111  axpre-suploc  8112  axlttrn  8238  axsuploc  8242  letri3  8250  letr  8252  le2add  8614  lt2add  8615  ltleadd  8616  lt2sub  8630  le2sub  8631  apreap  8757  apreim  8773  apti  8792  msq11  9072  dfinfre  9126  sup3exmid  9127  cju  9131  peano5nni  9136  1nn  9144  peano2nn  9145  nn2ge  9166  nominpos  9372  elz2  9541  dfuzi  9580  uzind  9581  supinfneg  9819  infsupneg  9820  elpqb  9874  xrletri3  10029  xrletr  10033  z2ge  10051  elixx1  10122  elioo2  10146  iooshf  10177  iooneg  10213  iccneg  10214  icoshft  10215  elfz1  10238  fzdifsuc  10306  fzrev  10309  1fv  10364  zsupcllemstep  10479  infssuzex  10483  nninfdcex  10487  zsupssdc  10488  exbtwnzlemstep  10497  exbtwnzlemshrink  10498  exbtwnzlemex  10499  exbtwnz  10500  rebtwn2zlemstep  10502  rebtwn2zlemshrink  10503  rebtwn2z  10504  qbtwnre  10506  qbtwnxr  10507  flval  10522  flqlelt  10526  flqbi  10540  flqbi2  10541  modqid2  10603  q2submod  10637  seqf1og  10773  nnesq  10911  hashunlem  11057  zfz1isolem1  11094  zfz1iso  11095  seq3coll  11096  fundm2domnop0  11099  pfxsuffeqwrdeq  11269  swrdpfx  11278  wrd2ind  11294  swrdccatin2  11300  swrdccatin2d  11315  pfxccatin12d  11316  reuccatpfxs1lem  11317  reuccatpfxs1  11318  shftlem  11367  shftfibg  11371  shftfib  11374  shftfn  11375  2shfti  11382  cjval  11396  cjth  11397  remim  11411  caucvgrelemcau  11531  caucvgre  11532  cvg1nlemcau  11535  cvg1nlemres  11536  rexanuz2  11542  recvguniq  11546  resqrexlemgt0  11571  resqrexlemoverl  11572  resqrexlemglsq  11573  resqrexlemsqa  11575  resqrexlemex  11576  rsqrmo  11578  resqrtcl  11580  rersqrtthlem  11581  absdiflt  11643  absdifle  11644  cau3lem  11665  icodiamlt  11731  maxleast  11764  negfi  11779  minmax  11781  lemininf  11785  ltmininf  11786  xrmaxlesup  11810  xrminmax  11816  xrltmininf  11821  xrlemininf  11822  iooinsup  11828  clim  11832  clim2  11834  climshftlemg  11853  addcn2  11861  climcau  11898  summodc  11934  fsum3  11938  fsum2dlemstep  11985  fisumcom2  11989  fsum00  12013  ntrivcvgap0  12100  prodeq1f  12103  prodeq2w  12107  prodeq2  12108  prodmodc  12129  zproddc  12130  fprodseq  12134  fprodntrivap  12135  fprod2dlemstep  12173  fprodcom2fi  12177  sin01bnd  12308  cos01bnd  12309  divalgmod  12478  ndvdssub  12481  gcdsupex  12518  gcdsupcl  12519  gcddvds  12524  dvdslegcd  12525  bezoutlemmain  12559  bezoutlemex  12562  bezoutlemzz  12563  bezoutlemeu  12568  bezoutlemle  12569  bezoutlemsup  12570  dfgcd3  12571  dfgcd2  12575  gcddiv  12580  lcmval  12625  lcmcllem  12629  dvdslcm  12631  lcmledvds  12632  lcmgcdlem  12639  lcmdvds  12641  coprmgcdb  12650  ncoprmgcdne1b  12651  coprmdvds1  12653  qredeu  12659  divgcdcoprm0  12663  divgcdcoprmex  12664  isprm3  12680  pw2dvdslemn  12727  pw2dvdseu  12730  oddpwdclemxy  12731  qnumdencl  12749  qnumdenbi  12754  crth  12786  reumodprminv  12816  pythagtriplem19  12845  pceu  12858  pczpre  12860  pcdiv  12865  pc11  12894  dvdsprmpweqle  12900  prmpwdvds  12918  pockthi  12921  infpnlem2  12923  elgz  12934  4sqlem12  12965  ennnfonelemim  13035  exmidunben  13037  ctinfom  13039  ctiunctlemu1st  13045  ctiunctlemu2nd  13046  ctiunctlemudc  13048  ctiunctlemfo  13050  infpn2  13067  ptex  13337  prdsval  13346  f1ocpbllem  13383  ercpbl  13404  erlecpbl  13405  grpidvalg  13446  grpidpropdg  13447  mgmlrid  13452  igsumvalx  13462  gsumfzval  13464  gsumress  13468  gsumval2  13470  issgrpd  13485  sgrppropd  13486  ismnddef  13491  sgrpidmndm  13493  ismndd  13510  mndpropd  13513  mndinvmod  13518  mnd1  13528  ismhm  13534  mhmex  13535  mhmpropd  13539  issubm  13545  insubm  13558  grppropd  13590  dfgrp2  13600  isgrpid2  13613  isgrpinv  13627  grplrinv  13630  grpidinv2  13631  grpidinv  13632  dfgrp3mlem  13671  grplactcnv  13675  releqgg  13797  eqgex  13798  eqgfval  13799  eqgval  13800  isghm  13820  ghmrn  13834  resghm  13837  ghmpropd  13860  cmnpropd  13872  ablpropd  13873  imasabl  13913  isrng  13937  rngdi  13943  rngdir  13944  rngpropd  13958  dfur2g  13965  issrg  13968  srgideu  13975  srgidmlem  13981  issrgid  13984  srg1zr  13990  isring  14003  ringideu  14020  ringidmlem  14025  isringid  14028  ringid  14029  ringpropd  14041  ring1  14062  oppr0g  14084  oppr1g  14085  dvdsrvald  14097  dvdsrd  14098  dvdsrtr  14105  unitgrp  14120  dvdsrpropdg  14151  unitpropdg  14152  rhmopp  14180  opprnzrbg  14189  opprsubrngg  14215  issubrg  14225  subrg1  14235  subrgugrp  14244  resrhm2b  14253  subrgpropd  14257  rhmpropd  14258  opprdomnbg  14278  aprval  14286  aprap  14290  islmod  14295  lmodlema  14296  islmodd  14297  lmodfopnelem2  14329  lmodprop2d  14352  islssm  14361  islssmg  14362  rnglidlrng  14502  isridl  14508  df2idl2rng  14512  quscrng  14537  istopg  14713  fiinbas  14763  eltg2  14767  topbas  14781  neiint  14859  neipsm  14868  opnneissb  14869  opnssneib  14870  innei  14877  restbasg  14882  iscnp4  14932  cnpnei  14933  cnconst2  14947  cnptopresti  14952  cnptoprest  14953  cnpdis  14956  lmss  14960  lmres  14962  txbas  14972  eltx  14973  neitx  14982  txcnp  14985  txcnmpt  14987  uptx  14988  txdis  14991  txdis1cn  14992  txlm  14993  txhmeo  15033  ispsmet  15037  ismet  15058  isxmet  15059  bldisj  15115  blininf  15138  blssexps  15143  blssex  15144  ssblex  15145  xmspropd  15191  mspropd  15192  neibl  15205  metequiv  15209  bdmopn  15218  metrest  15220  xmetxp  15221  xmetxpbl  15222  xmettx  15224  metcnp3  15225  tgioo  15268  tgqioo  15269  addcncntoplem  15275  mpomulcn  15280  mulcncflem  15321  dedekindeu  15337  dedekindicclemicc  15346  limccl  15373  ellimc3apf  15374  limcimolemlt  15378  limccoap  15392  elply2  15449  sin0pilem2  15496  sincosq1sgn  15540  sincosq2sgn  15541  sincosq3sgn  15542  sincosq4sgn  15543  perfect  15715  lgsval  15723  lgsdir2lem5  15751  lgsne0  15757  lgsquadlem1  15796  lgsquadlem2  15797  lgsquadlem3  15798  lgsquad  15799  2lgslem3  15820  2sqlem8a  15841  2sqlem8  15842  2sqlem9  15843  gropd  15888  grstructd2dom  15889  incistruhgr  15931  uhgr2edg  16045  vtxd0nedgbfi  16105  wlkeq  16151  istrl  16180  clwwlkn2  16216  eupthsg  16240  iseupth  16242  bj-sseq  16324  bj-charfunbi  16342  bj-nalset  16426  bj-indeq  16460  bj-2inf  16469  strcoll2  16514  strcollnft  16515  strcollnfALT  16517  sscoll2  16519  subctctexmid  16537  domomsubct  16538  exmidsbthrlem  16562  sbthom  16566  qdencn  16567  ltlenmkv  16610