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  1810  mopick  2120  clelab  2319  cbvrexfw  2717  cbvrexf  2719  cbvreu  2724  cbvrexvw  2731  cbvreuvw  2732  cbvrexdva2  2734  cbvrab  2758  gencbvex  2807  rspce  2860  eqvincf  2886  ceqsrexv  2891  elrabf  2915  rexab2  2927  reu2  2949  reu6  2950  rmo4  2954  reu8  2957  reuind  2966  sbcan  3029  sbcang  3030  sbcabel  3068  rmob  3079  cbvrexcsf  3145  cbvreucsf  3146  cbvrabcsf  3147  difjust  3155  injust  3159  eldif  3163  ssconb  3293  elin  3343  opeq1  3805  opeq2  3806  2ralunsn  3825  elunii  3841  csbunig  3844  eluniab  3848  cbvopab  4101  cbvopab1  4103  cbvopab2  4104  cbvopab1s  4105  cbvopab2v  4107  cbvmptf  4124  cbvmpt  4125  trel  4135  nalset  4160  elssabg  4178  mss  4256  exss  4257  opelopab2a  4296  poeq1  4331  pocl  4335  soeq1  4347  weeq1  4388  weeq2  4389  ordeq  4404  zfun  4466  snnex  4480  reusv3  4492  ontr2exmid  4558  regexmid  4568  onintexmid  4606  reg3exmid  4613  peano5  4631  limom  4647  nnregexmid  4654  vtoclr  4708  opeliunxp  4715  poinxp  4729  opbrop  4739  csbxpg  4741  opeliunxp2  4803  relop  4813  brcogw  4832  elrnmpt1  4914  elsnres  4980  dfres2  4995  inimasn  5084  xpcanm  5106  xpcan2m  5107  elxp4  5154  elxp5  5155  cnvsom  5210  sbcfung  5279  funopg  5289  fununi  5323  funcnvuni  5324  fneq1  5343  2elresin  5366  feq1  5387  sbcfng  5402  sbcfg  5403  f1eq1  5455  foeq1  5473  f1oeq1  5489  f1oeq2  5490  f1oeq3  5491  ffoss  5533  brprcneu  5548  fv3  5578  tz6.12f  5584  ssimaex  5619  fvopab3g  5631  fvopab3ig  5632  fvopab6  5655  fmptco  5725  elunirn  5810  f1imaeq  5819  foeqcnvco  5834  fliftfun  5840  fliftval  5844  isoeq1  5845  isoeq4  5848  isoini  5862  isopolem  5866  f1oiso2  5871  riotabidv  5876  cbvriota  5885  acexmid  5918  ovanraleqv  5943  cbvoprab1  5991  cbvoprab2  5992  cbvoprab12  5993  cbvmpox  5997  ov  6039  ovig  6041  ovg  6059  caovimo  6114  caoftrn  6160  opabex3d  6175  opabex3  6176  uchoice  6192  elxp6  6224  unielxp  6229  dfoprab4  6247  dfoprab4f  6248  fmpox  6255  xporderlem  6286  poxp  6287  cnvoprab  6289  f1od2  6290  opeliunxp2f  6293  rbropapd  6297  dftpos4  6318  tpostpos  6319  smoiso  6357  tfrlem3ag  6364  tfrlem3a  6365  tfr0dm  6377  tfrlemisucaccv  6380  tfrlemiex  6386  tfrlemi1  6387  tfrlemi14d  6388  tfrexlem  6389  tfr1onlem3ag  6392  tfr1onlemsucaccv  6396  tfr1onlemex  6402  tfr1onlemaccex  6403  tfr1onlemres  6404  tfrcllemsucaccv  6409  tfrcllembxssdm  6411  tfrcllemex  6415  tfrcllemaccex  6416  tfrcllemres  6417  tfrcldm  6418  frec0g  6452  frecabcl  6454  freccllem  6457  frecfcllem  6459  frecsuclem  6461  frecsuc  6462  nnacan  6567  nnmcan  6574  nnaordex  6583  ertr  6604  brecop  6681  eroveu  6682  ecopovtrn  6688  ecopovtrng  6691  th3qlem1  6693  th3qlem2  6694  th3q  6696  elpm2r  6722  mapsncnv  6751  elixp2  6758  ixpeq1  6765  elixpsn  6791  ixpsnf1o  6792  mapsnen  6867  map1  6868  xpsnen  6877  endisj  6880  pw2f1odclem  6892  xpf1o  6902  phplem3g  6914  ssfiexmid  6934  domfiexmid  6936  findcard2s  6948  isinfinf  6955  ac6sfi  6956  fiintim  6987  fisseneq  6990  opabfi  6994  f1dmvrnfibi  7005  sbthlem2  7019  isbth  7028  supeq1  7047  supeq3  7051  supeq123d  7052  supmoti  7054  eqsupti  7057  supsnti  7066  isotilem  7067  isoti  7068  supisolem  7069  supisoex  7070  cnvinfex  7079  cnvti  7080  eqinfti  7081  infvalti  7083  updjud  7143  ctssexmid  7211  omniwomnimkv  7228  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  acfun  7269  tapeq1  7314  tapeq2  7315  exmidapne  7322  ccfunen  7326  cc2lem  7328  cc3  7330  ltsopi  7382  recexnq  7452  recmulnqg  7453  ltsonq  7460  lt2addnq  7466  lt2mulnq  7467  ltbtwnnqq  7477  prarloclemarch2  7481  enq0sym  7494  enq0ref  7495  enq0tr  7496  enq0breq  7498  addnq0mo  7509  mulnq0mo  7510  addnnnq0  7511  mulnnnq0  7512  nqnq0a  7516  nqnq0m  7517  elinp  7536  prcdnql  7546  prcunqu  7547  prltlu  7549  prdisj  7554  prarloclemlo  7556  prarloclem3  7559  prarloclem5  7562  ltdfpr  7568  genprndl  7583  genprndu  7584  genpdisj  7585  appdivnq  7625  ltpopr  7657  ltexprlemdisj  7668  ltexprlemloc  7669  ltexprlemrl  7672  ltexprlemru  7674  ltexpri  7675  recexprlemm  7686  recexprlemdisj  7692  recexprlemloc  7693  recexprlem1ssl  7695  recexprlem1ssu  7696  recexpr  7700  aptiprleml  7701  archpr  7705  cauappcvgprlemladdru  7718  cauappcvgprlemladdrl  7719  cauappcvgprlem1  7721  cauappcvgprlemlim  7723  cauappcvgpr  7724  caucvgprlemnkj  7728  caucvgprlemnbj  7729  caucvgprlemcl  7738  caucvgpr  7744  caucvgprprlemcbv  7749  caucvgprprlemval  7750  caucvgprprlemopu  7761  caucvgprpr  7774  suplocexpr  7787  addsrmo  7805  mulsrmo  7806  addsrpr  7807  mulsrpr  7808  lttrsr  7824  recexgt0sr  7835  caucvgsrlemcau  7855  caucvgsrlemgt1  7857  caucvgsrlemoffcau  7860  caucvgsrlemoffres  7862  caucvgsr  7864  suplocsrlem  7870  ltresr  7901  pitonn  7910  peano1nnnn  7914  peano2nnnn  7915  axprecex  7942  axcnre  7943  axpre-lttrn  7946  peano5nnnn  7954  axcaucvglemcau  7960  axcaucvglemres  7961  axpre-suploclemres  7963  axpre-suploc  7964  axlttrn  8090  axsuploc  8094  letri3  8102  letr  8104  le2add  8465  lt2add  8466  ltleadd  8467  lt2sub  8481  le2sub  8482  apreap  8608  apreim  8624  apti  8643  msq11  8923  dfinfre  8977  sup3exmid  8978  cju  8982  peano5nni  8987  1nn  8995  peano2nn  8996  nn2ge  9017  nominpos  9223  elz2  9391  dfuzi  9430  uzind  9431  supinfneg  9663  infsupneg  9664  elpqb  9718  xrletri3  9873  xrletr  9877  z2ge  9895  elixx1  9966  elioo2  9990  iooshf  10021  iooneg  10057  iccneg  10058  icoshft  10059  elfz1  10082  fzdifsuc  10150  fzrev  10153  1fv  10208  exbtwnzlemstep  10319  exbtwnzlemshrink  10320  exbtwnzlemex  10321  exbtwnz  10322  rebtwn2zlemstep  10324  rebtwn2zlemshrink  10325  rebtwn2z  10326  qbtwnre  10328  qbtwnxr  10329  flval  10344  flqlelt  10348  flqbi  10362  flqbi2  10363  modqid2  10425  q2submod  10459  seqf1og  10595  nnesq  10733  hashunlem  10878  zfz1isolem1  10914  zfz1iso  10915  seq3coll  10916  shftlem  10963  shftfibg  10967  shftfib  10970  shftfn  10971  2shfti  10978  cjval  10992  cjth  10993  remim  11007  caucvgrelemcau  11127  caucvgre  11128  cvg1nlemcau  11131  cvg1nlemres  11132  rexanuz2  11138  recvguniq  11142  resqrexlemgt0  11167  resqrexlemoverl  11168  resqrexlemglsq  11169  resqrexlemsqa  11171  resqrexlemex  11172  rsqrmo  11174  resqrtcl  11176  rersqrtthlem  11177  absdiflt  11239  absdifle  11240  cau3lem  11261  icodiamlt  11327  maxleast  11360  negfi  11374  minmax  11376  lemininf  11380  ltmininf  11381  xrmaxlesup  11405  xrminmax  11411  xrltmininf  11416  xrlemininf  11417  iooinsup  11423  clim  11427  clim2  11429  climshftlemg  11448  addcn2  11456  climcau  11493  summodc  11529  fsum3  11533  fsum2dlemstep  11580  fisumcom2  11584  fsum00  11608  ntrivcvgap0  11695  prodeq1f  11698  prodeq2w  11702  prodeq2  11703  prodmodc  11724  zproddc  11725  fprodseq  11729  fprodntrivap  11730  fprod2dlemstep  11768  fprodcom2fi  11772  sin01bnd  11903  cos01bnd  11904  divalgmod  12071  ndvdssub  12074  zsupcllemstep  12085  infssuzex  12089  nninfdcex  12093  zsupssdc  12094  gcdsupex  12097  gcdsupcl  12098  gcddvds  12103  dvdslegcd  12104  bezoutlemmain  12138  bezoutlemex  12141  bezoutlemzz  12142  bezoutlemeu  12147  bezoutlemle  12148  bezoutlemsup  12149  dfgcd3  12150  dfgcd2  12154  gcddiv  12159  lcmval  12204  lcmcllem  12208  dvdslcm  12210  lcmledvds  12211  lcmgcdlem  12218  lcmdvds  12220  coprmgcdb  12229  ncoprmgcdne1b  12230  coprmdvds1  12232  qredeu  12238  divgcdcoprm0  12242  divgcdcoprmex  12243  isprm3  12259  pw2dvdslemn  12306  pw2dvdseu  12309  oddpwdclemxy  12310  qnumdencl  12328  qnumdenbi  12333  crth  12365  reumodprminv  12394  pythagtriplem19  12423  pceu  12436  pczpre  12438  pcdiv  12443  pc11  12472  dvdsprmpweqle  12478  prmpwdvds  12496  pockthi  12499  infpnlem2  12501  elgz  12512  4sqlem12  12543  ennnfonelemim  12584  exmidunben  12586  ctinfom  12588  ctiunctlemu1st  12594  ctiunctlemu2nd  12595  ctiunctlemudc  12597  ctiunctlemfo  12599  infpn2  12616  ptex  12878  f1ocpbllem  12896  ercpbl  12917  erlecpbl  12918  grpidvalg  12959  grpidpropdg  12960  mgmlrid  12965  igsumvalx  12975  gsumfzval  12977  gsumress  12981  gsumval2  12983  issgrpd  12998  sgrppropd  12999  ismnddef  13002  sgrpidmndm  13004  ismndd  13021  mndpropd  13024  mndinvmod  13029  mnd1  13030  ismhm  13036  mhmex  13037  mhmpropd  13041  issubm  13047  insubm  13060  grppropd  13092  dfgrp2  13102  isgrpid2  13115  isgrpinv  13129  grplrinv  13132  grpidinv2  13133  grpidinv  13134  dfgrp3mlem  13173  grplactcnv  13177  releqgg  13293  eqgex  13294  eqgfval  13295  eqgval  13296  isghm  13316  ghmrn  13330  resghm  13333  ghmpropd  13356  cmnpropd  13368  ablpropd  13369  imasabl  13409  isrng  13433  rngdi  13439  rngdir  13440  rngpropd  13454  dfur2g  13461  issrg  13464  srgideu  13471  srgidmlem  13477  issrgid  13480  srg1zr  13486  isring  13499  ringideu  13516  ringidmlem  13521  isringid  13524  ringid  13525  ringpropd  13537  ring1  13558  oppr0g  13580  oppr1g  13581  reldvdsrsrg  13591  dvdsrvald  13592  dvdsrd  13593  dvdsrtr  13600  unitgrp  13615  dvdsrpropdg  13646  unitpropdg  13647  rhmopp  13675  opprnzrbg  13684  opprsubrngg  13710  issubrg  13720  subrg1  13730  subrgugrp  13739  resrhm2b  13748  subrgpropd  13752  rhmpropd  13753  opprdomnbg  13773  aprval  13781  aprap  13785  islmod  13790  lmodlema  13791  islmodd  13792  lmodfopnelem2  13824  lmodprop2d  13847  islssm  13856  islssmg  13857  rnglidlrng  13997  isridl  14003  df2idl2rng  14007  quscrng  14032  istopg  14178  fiinbas  14228  eltg2  14232  topbas  14246  neiint  14324  neipsm  14333  opnneissb  14334  opnssneib  14335  innei  14342  restbasg  14347  iscnp4  14397  cnpnei  14398  cnconst2  14412  cnptopresti  14417  cnptoprest  14418  cnpdis  14421  lmss  14425  lmres  14427  txbas  14437  eltx  14438  neitx  14447  txcnp  14450  txcnmpt  14452  uptx  14453  txdis  14456  txdis1cn  14457  txlm  14458  txhmeo  14498  ispsmet  14502  ismet  14523  isxmet  14524  bldisj  14580  blininf  14603  blssexps  14608  blssex  14609  ssblex  14610  xmspropd  14656  mspropd  14657  neibl  14670  metequiv  14674  bdmopn  14683  metrest  14685  xmetxp  14686  xmetxpbl  14687  xmettx  14689  metcnp3  14690  tgioo  14733  tgqioo  14734  addcncntoplem  14740  mpomulcn  14745  mulcncflem  14786  dedekindeu  14802  dedekindicclemicc  14811  limccl  14838  ellimc3apf  14839  limcimolemlt  14843  limccoap  14857  elply2  14914  sin0pilem2  14958  sincosq1sgn  15002  sincosq2sgn  15003  sincosq3sgn  15004  sincosq4sgn  15005  lgsval  15161  lgsdir2lem5  15189  lgsne0  15195  lgsquadlem1  15234  lgsquadlem2  15235  lgsquadlem3  15236  lgsquad  15237  2lgslem3  15258  2sqlem8a  15279  2sqlem8  15280  2sqlem9  15281  bj-sseq  15354  bj-charfunbi  15373  bj-nalset  15457  bj-indeq  15491  bj-2inf  15500  strcoll2  15545  strcollnft  15546  strcollnfALT  15548  sscoll2  15550  subctctexmid  15561  exmidsbthrlem  15582  sbthom  15586  qdencn  15587  ltlenmkv  15630