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  2797  gencbvex  2847  rspce  2902  eqvincf  2928  ceqsrexv  2933  elrabf  2957  rexab2  2969  reu2  2991  reu6  2992  rmo4  2996  reu8  2999  reuind  3008  sbcan  3071  sbcang  3072  reu8nf  3110  sbcabel  3111  rmob  3122  cbvrexcsf  3188  cbvreucsf  3189  cbvrabcsf  3190  difjust  3198  injust  3202  eldif  3206  ssconb  3337  elin  3387  opeq1  3856  opeq2  3857  2ralunsn  3876  elunii  3892  csbunig  3895  eluniab  3899  cbvopab  4154  cbvopab1  4156  cbvopab2  4157  cbvopab1s  4158  cbvopab2v  4160  cbvmptf  4177  cbvmpt  4178  trel  4188  nalset  4213  elssabg  4231  mss  4311  exss  4312  opelopab2a  4352  poeq1  4389  pocl  4393  soeq1  4405  weeq1  4446  weeq2  4447  ordeq  4462  zfun  4524  snnex  4538  reusv3  4550  ontr2exmid  4616  regexmid  4626  onintexmid  4664  reg3exmid  4671  peano5  4689  limom  4705  nnregexmid  4712  vtoclr  4766  opeliunxp  4773  poinxp  4787  opbrop  4797  csbxpg  4799  opeliunxp2  4861  relop  4871  brcogw  4890  elrnmpt1  4974  elsnres  5041  dfres2  5056  inimasn  5145  xpcanm  5167  xpcan2m  5168  elxp4  5215  elxp5  5216  cnvsom  5271  sbcfung  5341  funopg  5351  fununi  5388  funcnvuni  5389  fneq1  5408  2elresin  5433  feq1  5455  sbcfng  5470  sbcfg  5471  f1eq1  5525  foeq1  5543  f1oeq1  5559  f1oeq2  5560  f1oeq3  5561  ffoss  5603  brprcneu  5619  fv3  5649  tz6.12f  5655  ssimaex  5694  fvopab3g  5706  fvopab3ig  5707  fvopab6  5730  fmptco  5800  funopsn  5816  funopdmsn  5818  elunirn  5889  f1imaeq  5898  foeqcnvco  5913  fliftfun  5919  fliftval  5923  isoeq1  5924  isoeq4  5927  isoini  5941  isopolem  5945  f1oiso2  5950  riotabidv  5955  cbvriotavw  5964  cbvriota  5965  acexmid  5999  ovanraleqv  6024  cbvoprab1  6075  cbvoprab2  6076  cbvoprab12  6077  cbvmpox  6081  ov  6123  ovig  6125  ovg  6143  caovimo  6198  caoftrn  6249  opabex3d  6264  opabex3  6265  uchoice  6281  elxp6  6313  unielxp  6318  dfoprab4  6336  dfoprab4f  6337  fmpox  6344  xporderlem  6375  poxp  6376  cnvoprab  6378  f1od2  6379  opeliunxp2f  6382  rbropapd  6386  dftpos4  6407  tpostpos  6408  smoiso  6446  tfrlem3ag  6453  tfrlem3a  6454  tfr0dm  6466  tfrlemisucaccv  6469  tfrlemiex  6475  tfrlemi1  6476  tfrlemi14d  6477  tfrexlem  6478  tfr1onlem3ag  6481  tfr1onlemsucaccv  6485  tfr1onlemex  6491  tfr1onlemaccex  6492  tfr1onlemres  6493  tfrcllemsucaccv  6498  tfrcllembxssdm  6500  tfrcllemex  6504  tfrcllemaccex  6505  tfrcllemres  6506  tfrcldm  6507  frec0g  6541  frecabcl  6543  freccllem  6546  frecfcllem  6548  frecsuclem  6550  frecsuc  6551  nnacan  6656  nnmcan  6663  nnaordex  6672  ertr  6693  brecop  6770  eroveu  6771  ecopovtrn  6777  ecopovtrng  6780  th3qlem1  6782  th3qlem2  6783  th3q  6785  elpm2r  6811  mapsncnv  6840  elixp2  6847  ixpeq1  6854  elixpsn  6880  ixpsnf1o  6881  mapsnen  6962  map1  6963  xpsnen  6976  endisj  6979  pw2f1odclem  6991  xpf1o  7001  phplem3g  7013  ssfiexmid  7034  domfiexmid  7036  findcard2s  7048  isinfinf  7055  ac6sfi  7056  fiintim  7089  fisseneq  7092  opabfi  7096  f1dmvrnfibi  7107  sbthlem2  7121  isbth  7130  supeq1  7149  supeq3  7153  supeq123d  7154  supmoti  7156  eqsupti  7159  supsnti  7168  isotilem  7169  isoti  7170  supisolem  7171  supisoex  7172  cnvinfex  7181  cnvti  7182  eqinfti  7183  infvalti  7185  updjud  7245  ctssexmid  7313  omniwomnimkv  7330  exmidfodomrlemr  7376  exmidfodomrlemrALT  7377  acneq  7380  acfun  7385  tapeq1  7434  tapeq2  7435  exmidapne  7442  ccfunen  7446  cc2lem  7448  cc3  7450  ltsopi  7503  recexnq  7573  recmulnqg  7574  ltsonq  7581  lt2addnq  7587  lt2mulnq  7588  ltbtwnnqq  7598  prarloclemarch2  7602  enq0sym  7615  enq0ref  7616  enq0tr  7617  enq0breq  7619  addnq0mo  7630  mulnq0mo  7631  addnnnq0  7632  mulnnnq0  7633  nqnq0a  7637  nqnq0m  7638  elinp  7657  prcdnql  7667  prcunqu  7668  prltlu  7670  prdisj  7675  prarloclemlo  7677  prarloclem3  7680  prarloclem5  7683  ltdfpr  7689  genprndl  7704  genprndu  7705  genpdisj  7706  appdivnq  7746  ltpopr  7778  ltexprlemdisj  7789  ltexprlemloc  7790  ltexprlemrl  7793  ltexprlemru  7795  ltexpri  7796  recexprlemm  7807  recexprlemdisj  7813  recexprlemloc  7814  recexprlem1ssl  7816  recexprlem1ssu  7817  recexpr  7821  aptiprleml  7822  archpr  7826  cauappcvgprlemladdru  7839  cauappcvgprlemladdrl  7840  cauappcvgprlem1  7842  cauappcvgprlemlim  7844  cauappcvgpr  7845  caucvgprlemnkj  7849  caucvgprlemnbj  7850  caucvgprlemcl  7859  caucvgpr  7865  caucvgprprlemcbv  7870  caucvgprprlemval  7871  caucvgprprlemopu  7882  caucvgprpr  7895  suplocexpr  7908  addsrmo  7926  mulsrmo  7927  addsrpr  7928  mulsrpr  7929  lttrsr  7945  recexgt0sr  7956  caucvgsrlemcau  7976  caucvgsrlemgt1  7978  caucvgsrlemoffcau  7981  caucvgsrlemoffres  7983  caucvgsr  7985  suplocsrlem  7991  ltresr  8022  pitonn  8031  peano1nnnn  8035  peano2nnnn  8036  axprecex  8063  axcnre  8064  axpre-lttrn  8067  peano5nnnn  8075  axcaucvglemcau  8081  axcaucvglemres  8082  axpre-suploclemres  8084  axpre-suploc  8085  axlttrn  8211  axsuploc  8215  letri3  8223  letr  8225  le2add  8587  lt2add  8588  ltleadd  8589  lt2sub  8603  le2sub  8604  apreap  8730  apreim  8746  apti  8765  msq11  9045  dfinfre  9099  sup3exmid  9100  cju  9104  peano5nni  9109  1nn  9117  peano2nn  9118  nn2ge  9139  nominpos  9345  elz2  9514  dfuzi  9553  uzind  9554  supinfneg  9786  infsupneg  9787  elpqb  9841  xrletri3  9996  xrletr  10000  z2ge  10018  elixx1  10089  elioo2  10113  iooshf  10144  iooneg  10180  iccneg  10181  icoshft  10182  elfz1  10205  fzdifsuc  10273  fzrev  10276  1fv  10331  zsupcllemstep  10444  infssuzex  10448  nninfdcex  10452  zsupssdc  10453  exbtwnzlemstep  10462  exbtwnzlemshrink  10463  exbtwnzlemex  10464  exbtwnz  10465  rebtwn2zlemstep  10467  rebtwn2zlemshrink  10468  rebtwn2z  10469  qbtwnre  10471  qbtwnxr  10472  flval  10487  flqlelt  10491  flqbi  10505  flqbi2  10506  modqid2  10568  q2submod  10602  seqf1og  10738  nnesq  10876  hashunlem  11021  zfz1isolem1  11057  zfz1iso  11058  seq3coll  11059  fundm2domnop0  11062  pfxsuffeqwrdeq  11225  swrdpfx  11234  wrd2ind  11250  swrdccatin2  11256  swrdccatin2d  11271  pfxccatin12d  11272  reuccatpfxs1lem  11273  reuccatpfxs1  11274  shftlem  11322  shftfibg  11326  shftfib  11329  shftfn  11330  2shfti  11337  cjval  11351  cjth  11352  remim  11366  caucvgrelemcau  11486  caucvgre  11487  cvg1nlemcau  11490  cvg1nlemres  11491  rexanuz2  11497  recvguniq  11501  resqrexlemgt0  11526  resqrexlemoverl  11527  resqrexlemglsq  11528  resqrexlemsqa  11530  resqrexlemex  11531  rsqrmo  11533  resqrtcl  11535  rersqrtthlem  11536  absdiflt  11598  absdifle  11599  cau3lem  11620  icodiamlt  11686  maxleast  11719  negfi  11734  minmax  11736  lemininf  11740  ltmininf  11741  xrmaxlesup  11765  xrminmax  11771  xrltmininf  11776  xrlemininf  11777  iooinsup  11783  clim  11787  clim2  11789  climshftlemg  11808  addcn2  11816  climcau  11853  summodc  11889  fsum3  11893  fsum2dlemstep  11940  fisumcom2  11944  fsum00  11968  ntrivcvgap0  12055  prodeq1f  12058  prodeq2w  12062  prodeq2  12063  prodmodc  12084  zproddc  12085  fprodseq  12089  fprodntrivap  12090  fprod2dlemstep  12128  fprodcom2fi  12132  sin01bnd  12263  cos01bnd  12264  divalgmod  12433  ndvdssub  12436  gcdsupex  12473  gcdsupcl  12474  gcddvds  12479  dvdslegcd  12480  bezoutlemmain  12514  bezoutlemex  12517  bezoutlemzz  12518  bezoutlemeu  12523  bezoutlemle  12524  bezoutlemsup  12525  dfgcd3  12526  dfgcd2  12530  gcddiv  12535  lcmval  12580  lcmcllem  12584  dvdslcm  12586  lcmledvds  12587  lcmgcdlem  12594  lcmdvds  12596  coprmgcdb  12605  ncoprmgcdne1b  12606  coprmdvds1  12608  qredeu  12614  divgcdcoprm0  12618  divgcdcoprmex  12619  isprm3  12635  pw2dvdslemn  12682  pw2dvdseu  12685  oddpwdclemxy  12686  qnumdencl  12704  qnumdenbi  12709  crth  12741  reumodprminv  12771  pythagtriplem19  12800  pceu  12813  pczpre  12815  pcdiv  12820  pc11  12849  dvdsprmpweqle  12855  prmpwdvds  12873  pockthi  12876  infpnlem2  12878  elgz  12889  4sqlem12  12920  ennnfonelemim  12990  exmidunben  12992  ctinfom  12994  ctiunctlemu1st  13000  ctiunctlemu2nd  13001  ctiunctlemudc  13003  ctiunctlemfo  13005  infpn2  13022  ptex  13292  prdsval  13301  f1ocpbllem  13338  ercpbl  13359  erlecpbl  13360  grpidvalg  13401  grpidpropdg  13402  mgmlrid  13407  igsumvalx  13417  gsumfzval  13419  gsumress  13423  gsumval2  13425  issgrpd  13440  sgrppropd  13441  ismnddef  13446  sgrpidmndm  13448  ismndd  13465  mndpropd  13468  mndinvmod  13473  mnd1  13483  ismhm  13489  mhmex  13490  mhmpropd  13494  issubm  13500  insubm  13513  grppropd  13545  dfgrp2  13555  isgrpid2  13568  isgrpinv  13582  grplrinv  13585  grpidinv2  13586  grpidinv  13587  dfgrp3mlem  13626  grplactcnv  13630  releqgg  13752  eqgex  13753  eqgfval  13754  eqgval  13755  isghm  13775  ghmrn  13789  resghm  13792  ghmpropd  13815  cmnpropd  13827  ablpropd  13828  imasabl  13868  isrng  13892  rngdi  13898  rngdir  13899  rngpropd  13913  dfur2g  13920  issrg  13923  srgideu  13930  srgidmlem  13936  issrgid  13939  srg1zr  13945  isring  13958  ringideu  13975  ringidmlem  13980  isringid  13983  ringid  13984  ringpropd  13996  ring1  14017  oppr0g  14039  oppr1g  14040  reldvdsrsrg  14050  dvdsrvald  14051  dvdsrd  14052  dvdsrtr  14059  unitgrp  14074  dvdsrpropdg  14105  unitpropdg  14106  rhmopp  14134  opprnzrbg  14143  opprsubrngg  14169  issubrg  14179  subrg1  14189  subrgugrp  14198  resrhm2b  14207  subrgpropd  14211  rhmpropd  14212  opprdomnbg  14232  aprval  14240  aprap  14244  islmod  14249  lmodlema  14250  islmodd  14251  lmodfopnelem2  14283  lmodprop2d  14306  islssm  14315  islssmg  14316  rnglidlrng  14456  isridl  14462  df2idl2rng  14466  quscrng  14491  istopg  14667  fiinbas  14717  eltg2  14721  topbas  14735  neiint  14813  neipsm  14822  opnneissb  14823  opnssneib  14824  innei  14831  restbasg  14836  iscnp4  14886  cnpnei  14887  cnconst2  14901  cnptopresti  14906  cnptoprest  14907  cnpdis  14910  lmss  14914  lmres  14916  txbas  14926  eltx  14927  neitx  14936  txcnp  14939  txcnmpt  14941  uptx  14942  txdis  14945  txdis1cn  14946  txlm  14947  txhmeo  14987  ispsmet  14991  ismet  15012  isxmet  15013  bldisj  15069  blininf  15092  blssexps  15097  blssex  15098  ssblex  15099  xmspropd  15145  mspropd  15146  neibl  15159  metequiv  15163  bdmopn  15172  metrest  15174  xmetxp  15175  xmetxpbl  15176  xmettx  15178  metcnp3  15179  tgioo  15222  tgqioo  15223  addcncntoplem  15229  mpomulcn  15234  mulcncflem  15275  dedekindeu  15291  dedekindicclemicc  15300  limccl  15327  ellimc3apf  15328  limcimolemlt  15332  limccoap  15346  elply2  15403  sin0pilem2  15450  sincosq1sgn  15494  sincosq2sgn  15495  sincosq3sgn  15496  sincosq4sgn  15497  perfect  15669  lgsval  15677  lgsdir2lem5  15705  lgsne0  15711  lgsquadlem1  15750  lgsquadlem2  15751  lgsquadlem3  15752  lgsquad  15753  2lgslem3  15774  2sqlem8a  15795  2sqlem8  15796  2sqlem9  15797  gropd  15842  grstructd2dom  15843  incistruhgr  15884  uhgr2edg  15998  bj-sseq  16114  bj-charfunbi  16132  bj-nalset  16216  bj-indeq  16250  bj-2inf  16259  strcoll2  16304  strcollnft  16305  strcollnfALT  16307  sscoll2  16309  subctctexmid  16325  domomsubct  16326  exmidsbthrlem  16349  sbthom  16353  qdencn  16354  ltlenmkv  16397