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  605  pm5.17dc  905  orbididc  955  3anbi123d  1323  xorbi2d  1391  xorbi1d  1392  drsb1  1813  mopick  2123  clelab  2322  cbvrexfw  2720  cbvrexf  2722  cbvreu  2727  cbvrexvw  2734  cbvreuvw  2735  cbvrexdva2  2737  cbvrab  2761  gencbvex  2810  rspce  2863  eqvincf  2889  ceqsrexv  2894  elrabf  2918  rexab2  2930  reu2  2952  reu6  2953  rmo4  2957  reu8  2960  reuind  2969  sbcan  3032  sbcang  3033  sbcabel  3071  rmob  3082  cbvrexcsf  3148  cbvreucsf  3149  cbvrabcsf  3150  difjust  3158  injust  3162  eldif  3166  ssconb  3297  elin  3347  opeq1  3809  opeq2  3810  2ralunsn  3829  elunii  3845  csbunig  3848  eluniab  3852  cbvopab  4105  cbvopab1  4107  cbvopab2  4108  cbvopab1s  4109  cbvopab2v  4111  cbvmptf  4128  cbvmpt  4129  trel  4139  nalset  4164  elssabg  4182  mss  4260  exss  4261  opelopab2a  4300  poeq1  4335  pocl  4339  soeq1  4351  weeq1  4392  weeq2  4393  ordeq  4408  zfun  4470  snnex  4484  reusv3  4496  ontr2exmid  4562  regexmid  4572  onintexmid  4610  reg3exmid  4617  peano5  4635  limom  4651  nnregexmid  4658  vtoclr  4712  opeliunxp  4719  poinxp  4733  opbrop  4743  csbxpg  4745  opeliunxp2  4807  relop  4817  brcogw  4836  elrnmpt1  4918  elsnres  4984  dfres2  4999  inimasn  5088  xpcanm  5110  xpcan2m  5111  elxp4  5158  elxp5  5159  cnvsom  5214  sbcfung  5283  funopg  5293  fununi  5327  funcnvuni  5328  fneq1  5347  2elresin  5370  feq1  5391  sbcfng  5406  sbcfg  5407  f1eq1  5459  foeq1  5477  f1oeq1  5493  f1oeq2  5494  f1oeq3  5495  ffoss  5537  brprcneu  5552  fv3  5582  tz6.12f  5588  ssimaex  5623  fvopab3g  5635  fvopab3ig  5636  fvopab6  5659  fmptco  5729  elunirn  5814  f1imaeq  5823  foeqcnvco  5838  fliftfun  5844  fliftval  5848  isoeq1  5849  isoeq4  5852  isoini  5866  isopolem  5870  f1oiso2  5875  riotabidv  5880  cbvriota  5889  acexmid  5922  ovanraleqv  5947  cbvoprab1  5995  cbvoprab2  5996  cbvoprab12  5997  cbvmpox  6001  ov  6043  ovig  6045  ovg  6063  caovimo  6118  caoftrn  6164  opabex3d  6179  opabex3  6180  uchoice  6196  elxp6  6228  unielxp  6233  dfoprab4  6251  dfoprab4f  6252  fmpox  6259  xporderlem  6290  poxp  6291  cnvoprab  6293  f1od2  6294  opeliunxp2f  6297  rbropapd  6301  dftpos4  6322  tpostpos  6323  smoiso  6361  tfrlem3ag  6368  tfrlem3a  6369  tfr0dm  6381  tfrlemisucaccv  6384  tfrlemiex  6390  tfrlemi1  6391  tfrlemi14d  6392  tfrexlem  6393  tfr1onlem3ag  6396  tfr1onlemsucaccv  6400  tfr1onlemex  6406  tfr1onlemaccex  6407  tfr1onlemres  6408  tfrcllemsucaccv  6413  tfrcllembxssdm  6415  tfrcllemex  6419  tfrcllemaccex  6420  tfrcllemres  6421  tfrcldm  6422  frec0g  6456  frecabcl  6458  freccllem  6461  frecfcllem  6463  frecsuclem  6465  frecsuc  6466  nnacan  6571  nnmcan  6578  nnaordex  6587  ertr  6608  brecop  6685  eroveu  6686  ecopovtrn  6692  ecopovtrng  6695  th3qlem1  6697  th3qlem2  6698  th3q  6700  elpm2r  6726  mapsncnv  6755  elixp2  6762  ixpeq1  6769  elixpsn  6795  ixpsnf1o  6796  mapsnen  6871  map1  6872  xpsnen  6881  endisj  6884  pw2f1odclem  6896  xpf1o  6906  phplem3g  6918  ssfiexmid  6938  domfiexmid  6940  findcard2s  6952  isinfinf  6959  ac6sfi  6960  fiintim  6993  fisseneq  6996  opabfi  7000  f1dmvrnfibi  7011  sbthlem2  7025  isbth  7034  supeq1  7053  supeq3  7057  supeq123d  7058  supmoti  7060  eqsupti  7063  supsnti  7072  isotilem  7073  isoti  7074  supisolem  7075  supisoex  7076  cnvinfex  7085  cnvti  7086  eqinfti  7087  infvalti  7089  updjud  7149  ctssexmid  7217  omniwomnimkv  7234  exmidfodomrlemr  7271  exmidfodomrlemrALT  7272  acfun  7276  tapeq1  7321  tapeq2  7322  exmidapne  7329  ccfunen  7333  cc2lem  7335  cc3  7337  ltsopi  7389  recexnq  7459  recmulnqg  7460  ltsonq  7467  lt2addnq  7473  lt2mulnq  7474  ltbtwnnqq  7484  prarloclemarch2  7488  enq0sym  7501  enq0ref  7502  enq0tr  7503  enq0breq  7505  addnq0mo  7516  mulnq0mo  7517  addnnnq0  7518  mulnnnq0  7519  nqnq0a  7523  nqnq0m  7524  elinp  7543  prcdnql  7553  prcunqu  7554  prltlu  7556  prdisj  7561  prarloclemlo  7563  prarloclem3  7566  prarloclem5  7569  ltdfpr  7575  genprndl  7590  genprndu  7591  genpdisj  7592  appdivnq  7632  ltpopr  7664  ltexprlemdisj  7675  ltexprlemloc  7676  ltexprlemrl  7679  ltexprlemru  7681  ltexpri  7682  recexprlemm  7693  recexprlemdisj  7699  recexprlemloc  7700  recexprlem1ssl  7702  recexprlem1ssu  7703  recexpr  7707  aptiprleml  7708  archpr  7712  cauappcvgprlemladdru  7725  cauappcvgprlemladdrl  7726  cauappcvgprlem1  7728  cauappcvgprlemlim  7730  cauappcvgpr  7731  caucvgprlemnkj  7735  caucvgprlemnbj  7736  caucvgprlemcl  7745  caucvgpr  7751  caucvgprprlemcbv  7756  caucvgprprlemval  7757  caucvgprprlemopu  7768  caucvgprpr  7781  suplocexpr  7794  addsrmo  7812  mulsrmo  7813  addsrpr  7814  mulsrpr  7815  lttrsr  7831  recexgt0sr  7842  caucvgsrlemcau  7862  caucvgsrlemgt1  7864  caucvgsrlemoffcau  7867  caucvgsrlemoffres  7869  caucvgsr  7871  suplocsrlem  7877  ltresr  7908  pitonn  7917  peano1nnnn  7921  peano2nnnn  7922  axprecex  7949  axcnre  7950  axpre-lttrn  7953  peano5nnnn  7961  axcaucvglemcau  7967  axcaucvglemres  7968  axpre-suploclemres  7970  axpre-suploc  7971  axlttrn  8097  axsuploc  8101  letri3  8109  letr  8111  le2add  8473  lt2add  8474  ltleadd  8475  lt2sub  8489  le2sub  8490  apreap  8616  apreim  8632  apti  8651  msq11  8931  dfinfre  8985  sup3exmid  8986  cju  8990  peano5nni  8995  1nn  9003  peano2nn  9004  nn2ge  9025  nominpos  9231  elz2  9399  dfuzi  9438  uzind  9439  supinfneg  9671  infsupneg  9672  elpqb  9726  xrletri3  9881  xrletr  9885  z2ge  9903  elixx1  9974  elioo2  9998  iooshf  10029  iooneg  10065  iccneg  10066  icoshft  10067  elfz1  10090  fzdifsuc  10158  fzrev  10161  1fv  10216  zsupcllemstep  10321  infssuzex  10325  nninfdcex  10329  zsupssdc  10330  exbtwnzlemstep  10339  exbtwnzlemshrink  10340  exbtwnzlemex  10341  exbtwnz  10342  rebtwn2zlemstep  10344  rebtwn2zlemshrink  10345  rebtwn2z  10346  qbtwnre  10348  qbtwnxr  10349  flval  10364  flqlelt  10368  flqbi  10382  flqbi2  10383  modqid2  10445  q2submod  10479  seqf1og  10615  nnesq  10753  hashunlem  10898  zfz1isolem1  10934  zfz1iso  10935  seq3coll  10936  shftlem  10983  shftfibg  10987  shftfib  10990  shftfn  10991  2shfti  10998  cjval  11012  cjth  11013  remim  11027  caucvgrelemcau  11147  caucvgre  11148  cvg1nlemcau  11151  cvg1nlemres  11152  rexanuz2  11158  recvguniq  11162  resqrexlemgt0  11187  resqrexlemoverl  11188  resqrexlemglsq  11189  resqrexlemsqa  11191  resqrexlemex  11192  rsqrmo  11194  resqrtcl  11196  rersqrtthlem  11197  absdiflt  11259  absdifle  11260  cau3lem  11281  icodiamlt  11347  maxleast  11380  negfi  11395  minmax  11397  lemininf  11401  ltmininf  11402  xrmaxlesup  11426  xrminmax  11432  xrltmininf  11437  xrlemininf  11438  iooinsup  11444  clim  11448  clim2  11450  climshftlemg  11469  addcn2  11477  climcau  11514  summodc  11550  fsum3  11554  fsum2dlemstep  11601  fisumcom2  11605  fsum00  11629  ntrivcvgap0  11716  prodeq1f  11719  prodeq2w  11723  prodeq2  11724  prodmodc  11745  zproddc  11746  fprodseq  11750  fprodntrivap  11751  fprod2dlemstep  11789  fprodcom2fi  11793  sin01bnd  11924  cos01bnd  11925  divalgmod  12094  ndvdssub  12097  gcdsupex  12134  gcdsupcl  12135  gcddvds  12140  dvdslegcd  12141  bezoutlemmain  12175  bezoutlemex  12178  bezoutlemzz  12179  bezoutlemeu  12184  bezoutlemle  12185  bezoutlemsup  12186  dfgcd3  12187  dfgcd2  12191  gcddiv  12196  lcmval  12241  lcmcllem  12245  dvdslcm  12247  lcmledvds  12248  lcmgcdlem  12255  lcmdvds  12257  coprmgcdb  12266  ncoprmgcdne1b  12267  coprmdvds1  12269  qredeu  12275  divgcdcoprm0  12279  divgcdcoprmex  12280  isprm3  12296  pw2dvdslemn  12343  pw2dvdseu  12346  oddpwdclemxy  12347  qnumdencl  12365  qnumdenbi  12370  crth  12402  reumodprminv  12432  pythagtriplem19  12461  pceu  12474  pczpre  12476  pcdiv  12481  pc11  12510  dvdsprmpweqle  12516  prmpwdvds  12534  pockthi  12537  infpnlem2  12539  elgz  12550  4sqlem12  12581  ennnfonelemim  12651  exmidunben  12653  ctinfom  12655  ctiunctlemu1st  12661  ctiunctlemu2nd  12662  ctiunctlemudc  12664  ctiunctlemfo  12666  infpn2  12683  ptex  12945  f1ocpbllem  12963  ercpbl  12984  erlecpbl  12985  grpidvalg  13026  grpidpropdg  13027  mgmlrid  13032  igsumvalx  13042  gsumfzval  13044  gsumress  13048  gsumval2  13050  issgrpd  13065  sgrppropd  13066  ismnddef  13069  sgrpidmndm  13071  ismndd  13088  mndpropd  13091  mndinvmod  13096  mnd1  13097  ismhm  13103  mhmex  13104  mhmpropd  13108  issubm  13114  insubm  13127  grppropd  13159  dfgrp2  13169  isgrpid2  13182  isgrpinv  13196  grplrinv  13199  grpidinv2  13200  grpidinv  13201  dfgrp3mlem  13240  grplactcnv  13244  releqgg  13360  eqgex  13361  eqgfval  13362  eqgval  13363  isghm  13383  ghmrn  13397  resghm  13400  ghmpropd  13423  cmnpropd  13435  ablpropd  13436  imasabl  13476  isrng  13500  rngdi  13506  rngdir  13507  rngpropd  13521  dfur2g  13528  issrg  13531  srgideu  13538  srgidmlem  13544  issrgid  13547  srg1zr  13553  isring  13566  ringideu  13583  ringidmlem  13588  isringid  13591  ringid  13592  ringpropd  13604  ring1  13625  oppr0g  13647  oppr1g  13648  reldvdsrsrg  13658  dvdsrvald  13659  dvdsrd  13660  dvdsrtr  13667  unitgrp  13682  dvdsrpropdg  13713  unitpropdg  13714  rhmopp  13742  opprnzrbg  13751  opprsubrngg  13777  issubrg  13787  subrg1  13797  subrgugrp  13806  resrhm2b  13815  subrgpropd  13819  rhmpropd  13820  opprdomnbg  13840  aprval  13848  aprap  13852  islmod  13857  lmodlema  13858  islmodd  13859  lmodfopnelem2  13891  lmodprop2d  13914  islssm  13923  islssmg  13924  rnglidlrng  14064  isridl  14070  df2idl2rng  14074  quscrng  14099  istopg  14245  fiinbas  14295  eltg2  14299  topbas  14313  neiint  14391  neipsm  14400  opnneissb  14401  opnssneib  14402  innei  14409  restbasg  14414  iscnp4  14464  cnpnei  14465  cnconst2  14479  cnptopresti  14484  cnptoprest  14485  cnpdis  14488  lmss  14492  lmres  14494  txbas  14504  eltx  14505  neitx  14514  txcnp  14517  txcnmpt  14519  uptx  14520  txdis  14523  txdis1cn  14524  txlm  14525  txhmeo  14565  ispsmet  14569  ismet  14590  isxmet  14591  bldisj  14647  blininf  14670  blssexps  14675  blssex  14676  ssblex  14677  xmspropd  14723  mspropd  14724  neibl  14737  metequiv  14741  bdmopn  14750  metrest  14752  xmetxp  14753  xmetxpbl  14754  xmettx  14756  metcnp3  14757  tgioo  14800  tgqioo  14801  addcncntoplem  14807  mpomulcn  14812  mulcncflem  14853  dedekindeu  14869  dedekindicclemicc  14878  limccl  14905  ellimc3apf  14906  limcimolemlt  14910  limccoap  14924  elply2  14981  sin0pilem2  15028  sincosq1sgn  15072  sincosq2sgn  15073  sincosq3sgn  15074  sincosq4sgn  15075  perfect  15247  lgsval  15255  lgsdir2lem5  15283  lgsne0  15289  lgsquadlem1  15328  lgsquadlem2  15329  lgsquadlem3  15330  lgsquad  15331  2lgslem3  15352  2sqlem8a  15373  2sqlem8  15374  2sqlem9  15375  bj-sseq  15448  bj-charfunbi  15467  bj-nalset  15551  bj-indeq  15585  bj-2inf  15594  strcoll2  15639  strcollnft  15640  strcollnfALT  15642  sscoll2  15644  subctctexmid  15655  exmidsbthrlem  15676  sbthom  15680  qdencn  15681  ltlenmkv  15724