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  609  pm5.17dc  912  orbididc  962  ifpbi123d  1001  3anbi123d  1349  xorbi2d  1425  xorbi1d  1426  drsb1  1848  mopick  2159  clelab  2360  cbvrmow  2727  cbvrexfw  2768  cbvrexf  2770  cbvreu  2776  cbvrexvw  2783  cbvreuvw  2784  cbvrexdva2  2786  cbvrab  2811  gencbvex  2861  rspce  2916  eqvincf  2942  ceqsrexv  2947  elrabf  2971  rexab2  2983  reu2  3005  reu6  3006  rmo4  3010  reu8  3013  reuind  3022  sbcan  3085  sbcang  3086  reu8nf  3124  sbcabel  3125  rmob  3136  cbvrexcsf  3202  cbvreucsf  3203  cbvrabcsf  3204  difjust  3212  injust  3216  eldif  3220  ssconb  3352  elin  3402  opeq1  3883  opeq2  3884  2ralunsn  3903  elunii  3919  csbunig  3922  eluniab  3926  cbvopab  4181  cbvopab1  4183  cbvopab2  4184  cbvopab1s  4185  cbvopab2v  4187  cbvmptf  4204  cbvmpt  4205  trel  4215  nalset  4240  elssabg  4260  mss  4342  exss  4343  opelopab2a  4383  poeq1  4420  pocl  4424  soeq1  4436  weeq1  4477  weeq2  4478  ordeq  4493  zfun  4555  snnex  4569  reusv3  4581  ontr2exmid  4647  regexmid  4657  onintexmid  4695  reg3exmid  4702  peano5  4720  limom  4736  nnregexmid  4743  vtoclr  4798  opeliunxp  4805  poinxp  4819  opbrop  4829  csbxpg  4831  opeliunxp2  4895  relop  4905  brcogw  4924  elrnmpt1  5008  elsnres  5075  dfres2  5090  inimasn  5180  xpcanm  5202  xpcan2m  5203  elxp4  5250  elxp5  5251  cnvsom  5306  sbcfung  5376  funopg  5386  fununi  5424  funcnvuni  5425  fneq1  5444  2elresin  5469  feq1  5491  sbcfng  5506  sbcfg  5507  f1eq1  5568  foeq1  5586  f1oeq1  5602  f1oeq2  5603  f1oeq3  5604  ffoss  5647  brprcneu  5663  fv3  5693  tz6.12f  5699  ssimaex  5738  fvopab3g  5750  fvopab3ig  5751  fvopab6  5774  fmptco  5843  fsn2g  5852  funopsn  5860  funopdmsn  5864  elunirn  5939  f1imaeq  5948  foeqcnvco  5963  fliftfun  5969  fliftval  5973  isoeq1  5974  isoeq4  5977  isoini  5991  isopolem  5995  f1oiso2  6000  riotabidv  6005  cbvriotavw  6014  cbvriota  6015  acexmid  6049  ovanraleqv  6074  cbvoprab1  6125  cbvoprab2  6126  cbvoprab12  6127  cbvmpox  6131  ov  6173  ovig  6175  ovg  6193  caovimo  6248  caoftrn  6299  opabex3d  6314  opabex3  6315  uchoice  6331  elxp6  6363  unielxp  6368  dfoprab4  6386  dfoprab4f  6387  fmpox  6396  xporderlem  6427  poxp  6428  cnvoprab  6430  f1od2  6431  opeliunxp2f  6469  rbropapd  6473  dftpos4  6494  tpostpos  6495  smoiso  6533  tfrlem3ag  6540  tfrlem3a  6541  tfr0dm  6553  tfrlemisucaccv  6556  tfrlemiex  6562  tfrlemi1  6563  tfrlemi14d  6564  tfrexlem  6565  tfr1onlem3ag  6568  tfr1onlemsucaccv  6572  tfr1onlemex  6578  tfr1onlemaccex  6579  tfr1onlemres  6580  tfrcllemsucaccv  6585  tfrcllembxssdm  6587  tfrcllemex  6591  tfrcllemaccex  6592  tfrcllemres  6593  tfrcldm  6594  frec0g  6628  frecabcl  6630  freccllem  6633  frecfcllem  6635  frecsuclem  6637  frecsuc  6638  nnacan  6745  nnmcan  6752  nnaordex  6761  ertr  6782  brecop  6859  eroveu  6860  ecopovtrn  6866  ecopovtrng  6869  th3qlem1  6871  th3qlem2  6872  th3q  6874  elpm2r  6900  mapsncnv  6930  elixp2  6937  ixpeq1  6944  elixpsn  6970  ixpsnf1o  6971  mapsnend  7052  mapsnen  7053  map1  7054  xpsnen  7072  endisj  7075  pw2f1odclem  7087  xpf1o  7097  mapunen  7104  phplem3g  7110  ssfiexmid  7131  ssfiexmidt  7133  domfiexmid  7135  findcard2s  7147  isinfinf  7154  ac6sfi  7155  fiintim  7191  fisseneq  7195  opabfi  7200  f1dmvrnfibi  7211  sbthlem2  7228  isbth  7237  isfsupp  7242  supeq1  7277  supeq3  7281  supeq123d  7282  supmoti  7284  eqsupti  7287  supsnti  7296  isotilem  7297  isoti  7298  supisolem  7299  supisoex  7300  cnvinfex  7309  cnvti  7310  eqinfti  7311  infvalti  7313  updjud  7373  ctssexmid  7441  omniwomnimkv  7458  exmidfodomrlemr  7505  exmidfodomrlemrALT  7506  acneq  7509  acfun  7514  tapeq1  7566  tapeq2  7567  exmidapne  7574  ccfunen  7578  cc2lem  7580  cc3  7582  ltsopi  7635  recexnq  7705  recmulnqg  7706  ltsonq  7713  lt2addnq  7719  lt2mulnq  7720  ltbtwnnqq  7730  prarloclemarch2  7734  enq0sym  7747  enq0ref  7748  enq0tr  7749  enq0breq  7751  addnq0mo  7762  mulnq0mo  7763  addnnnq0  7764  mulnnnq0  7765  nqnq0a  7769  nqnq0m  7770  elinp  7789  prcdnql  7799  prcunqu  7800  prltlu  7802  prdisj  7807  prarloclemlo  7809  prarloclem3  7812  prarloclem5  7815  ltdfpr  7821  genprndl  7836  genprndu  7837  genpdisj  7838  appdivnq  7878  ltpopr  7910  ltexprlemdisj  7921  ltexprlemloc  7922  ltexprlemrl  7925  ltexprlemru  7927  ltexpri  7928  recexprlemm  7939  recexprlemdisj  7945  recexprlemloc  7946  recexprlem1ssl  7948  recexprlem1ssu  7949  recexpr  7953  aptiprleml  7954  archpr  7958  cauappcvgprlemladdru  7971  cauappcvgprlemladdrl  7972  cauappcvgprlem1  7974  cauappcvgprlemlim  7976  cauappcvgpr  7977  caucvgprlemnkj  7981  caucvgprlemnbj  7982  caucvgprlemcl  7991  caucvgpr  7997  caucvgprprlemcbv  8002  caucvgprprlemval  8003  caucvgprprlemopu  8014  caucvgprpr  8027  suplocexpr  8040  addsrmo  8058  mulsrmo  8059  addsrpr  8060  mulsrpr  8061  lttrsr  8077  recexgt0sr  8088  caucvgsrlemcau  8108  caucvgsrlemgt1  8110  caucvgsrlemoffcau  8113  caucvgsrlemoffres  8115  caucvgsr  8117  suplocsrlem  8123  ltresr  8154  pitonn  8163  peano1nnnn  8167  peano2nnnn  8168  axprecex  8195  axcnre  8196  axpre-lttrn  8199  peano5nnnn  8207  axcaucvglemcau  8213  axcaucvglemres  8214  axpre-suploclemres  8216  axpre-suploc  8217  axlttrn  8342  axsuploc  8346  letri3  8354  letr  8356  le2add  8718  lt2add  8719  ltleadd  8720  lt2sub  8734  le2sub  8735  apreap  8861  apreim  8877  apti  8896  msq11  9176  dfinfre  9230  sup3exmid  9231  cju  9235  peano5nni  9240  1nn  9248  peano2nn  9249  nn2ge  9270  nominpos  9476  elz2  9649  dfuzi  9688  uzind  9689  supinfneg  9927  infsupneg  9928  elpqb  9982  xrletri3  10137  xrletr  10141  z2ge  10159  elixx1  10230  elioo2  10254  iooshf  10285  iooneg  10321  iccneg  10322  icoshft  10323  elfz1  10347  fzdifsuc  10415  fzrev  10418  1fv  10473  zsupcllemstep  10589  infssuzex  10593  nninfdcex  10597  zsupssdc  10598  exbtwnzlemstep  10607  exbtwnzlemshrink  10608  exbtwnzlemex  10609  exbtwnz  10610  rebtwn2zlemstep  10612  rebtwn2zlemshrink  10613  rebtwn2z  10614  qbtwnre  10616  qbtwnxr  10617  flval  10632  flqlelt  10636  flqbi  10650  flqbi2  10651  modqid2  10713  q2submod  10747  seqf1og  10883  nnesq  11021  hashunlem  11168  hashfibclem  11206  zfz1isolem1  11212  zfz1iso  11213  seq3coll  11214  fundm2domnop0  11220  pfxsuffeqwrdeq  11390  swrdpfx  11399  wrd2ind  11415  swrdccatin2  11421  swrdccatin2d  11436  pfxccatin12d  11437  reuccatpfxs1lem  11438  reuccatpfxs1  11439  shftlem  11501  shftfibg  11505  shftfib  11508  shftfn  11509  2shfti  11516  cjval  11530  cjth  11531  remim  11545  caucvgrelemcau  11665  caucvgre  11666  cvg1nlemcau  11669  cvg1nlemres  11670  rexanuz2  11676  recvguniq  11680  resqrexlemgt0  11705  resqrexlemoverl  11706  resqrexlemglsq  11707  resqrexlemsqa  11709  resqrexlemex  11710  rsqrmo  11712  resqrtcl  11714  rersqrtthlem  11715  absdiflt  11777  absdifle  11778  cau3lem  11799  icodiamlt  11865  maxleast  11898  negfi  11913  minmax  11915  lemininf  11919  ltmininf  11920  xrmaxlesup  11944  xrminmax  11950  xrltmininf  11955  xrlemininf  11956  iooinsup  11962  clim  11966  clim2  11968  climshftlemg  11987  addcn2  11995  climcau  12032  summodc  12069  fsum3  12073  fsum2dlemstep  12120  fisumcom2  12124  fsum00  12148  ntrivcvgap0  12235  prodeq1f  12238  prodeq2w  12242  prodeq2  12243  prodmodc  12264  zproddc  12265  fprodseq  12269  fprodntrivap  12270  fprod2dlemstep  12308  fprodcom2fi  12312  sin01bnd  12443  cos01bnd  12444  divalgmod  12613  ndvdssub  12616  gcdsupex  12653  gcdsupcl  12654  gcddvds  12659  dvdslegcd  12660  bezoutlemmain  12694  bezoutlemex  12697  bezoutlemzz  12698  bezoutlemeu  12703  bezoutlemle  12704  bezoutlemsup  12705  dfgcd3  12706  dfgcd2  12710  gcddiv  12715  lcmval  12760  lcmcllem  12764  dvdslcm  12766  lcmledvds  12767  lcmgcdlem  12774  lcmdvds  12776  coprmgcdb  12785  ncoprmgcdne1b  12786  coprmdvds1  12788  qredeu  12794  divgcdcoprm0  12798  divgcdcoprmex  12799  isprm3  12815  pw2dvdslemn  12862  pw2dvdseu  12865  oddpwdclemxy  12866  qnumdencl  12884  qnumdenbi  12889  crth  12921  reumodprminv  12951  pythagtriplem19  12980  pceu  12993  pczpre  12995  pcdiv  13000  pc11  13029  dvdsprmpweqle  13035  prmpwdvds  13053  pockthi  13056  infpnlem2  13058  elgz  13069  4sqlem12  13100  ennnfonelemim  13175  exmidunben  13177  ctinfom  13179  ctiunctlemu1st  13185  ctiunctlemu2nd  13186  ctiunctlemudc  13188  ctiunctlemfo  13190  infpn2  13207  ptex  13477  prdsval  13486  f1ocpbllem  13523  ercpbl  13544  erlecpbl  13545  grpidvalg  13586  grpidpropdg  13587  mgmlrid  13592  igsumvalx  13602  gsumfzval  13604  gsumress  13608  gsumval2  13610  issgrpd  13625  sgrppropd  13626  ismnddef  13631  sgrpidmndm  13633  ismndd  13650  mndpropd  13653  mndinvmod  13658  mnd1  13668  ismhm  13674  mhmex  13675  mhmpropd  13679  issubm  13685  insubm  13698  grppropd  13730  dfgrp2  13740  isgrpid2  13753  isgrpinv  13767  grplrinv  13770  grpidinv2  13771  grpidinv  13772  dfgrp3mlem  13811  grplactcnv  13815  releqgg  13937  eqgex  13938  eqgfval  13939  eqgval  13940  isghm  13960  ghmrn  13974  resghm  13977  ghmpropd  14000  cmnpropd  14012  ablpropd  14013  imasabl  14053  isrng  14078  rngdi  14084  rngdir  14085  rngpropd  14099  dfur2g  14106  issrg  14109  srgideu  14116  srgidmlem  14122  issrgid  14125  srg1zr  14131  isring  14144  ringideu  14161  ringidmlem  14166  isringid  14169  ringid  14170  ringpropd  14182  ring1  14203  oppr0g  14225  oppr1g  14226  dvdsrvald  14238  dvdsrd  14239  dvdsrtr  14246  unitgrp  14261  dvdsrpropdg  14292  unitpropdg  14293  rhmopp  14321  opprnzrbg  14330  opprsubrngg  14356  issubrg  14366  subrg1  14376  subrgugrp  14385  resrhm2b  14394  subrgpropd  14398  rhmpropd  14399  opprdomnbg  14420  aprval  14428  aprap  14432  islmod  14439  lmodlema  14440  islmodd  14441  lmodfopnelem2  14473  lmodprop2d  14496  islssm  14505  islssmg  14506  rnglidlrng  14646  isridl  14652  df2idl2rng  14656  quscrng  14681  istopg  14864  fiinbas  14914  eltg2  14918  topbas  14932  neiint  15010  neipsm  15019  opnneissb  15020  opnssneib  15021  innei  15028  restbasg  15033  iscnp4  15083  cnpnei  15084  cnconst2  15098  cnptopresti  15103  cnptoprest  15104  cnpdis  15107  lmss  15111  lmres  15113  txbas  15123  eltx  15124  neitx  15133  txcnp  15136  txcnmpt  15138  uptx  15139  txdis  15142  txdis1cn  15143  txlm  15144  txhmeo  15184  ispsmet  15188  ismet  15209  isxmet  15210  bldisj  15266  blininf  15289  blssexps  15294  blssex  15295  ssblex  15296  xmspropd  15342  mspropd  15343  neibl  15356  metequiv  15360  bdmopn  15369  metrest  15371  xmetxp  15372  xmetxpbl  15373  xmettx  15375  metcnp3  15376  tgioo  15419  tgqioo  15420  addcncntoplem  15426  mpomulcn  15431  mulcncflem  15472  dedekindeu  15488  dedekindicclemicc  15497  limccl  15524  ellimc3apf  15525  limcimolemlt  15529  limccoap  15543  elply2  15600  sin0pilem2  15647  sincosq1sgn  15691  sincosq2sgn  15692  sincosq3sgn  15693  sincosq4sgn  15694  pellexlem3  15847  perfect  15869  lgsval  15877  lgsdir2lem5  15905  lgsne0  15911  lgsquadlem1  15950  lgsquadlem2  15951  lgsquadlem3  15952  lgsquad  15953  2lgslem3  15974  2sqlem8a  15995  2sqlem8  15996  2sqlem9  15997  gropd  16042  grstructd2dom  16043  incistruhgr  16085  uhgr2edg  16201  vtxd0nedgbfi  16294  wlkeq  16349  istrl  16380  clwwlkn2  16416  eupthsg  16440  iseupth  16442  eupth2lem1  16453  depind  16504  bj-sseq  16564  bj-charfunbi  16581  bj-nalset  16665  bj-indeq  16699  bj-2inf  16708  strcoll2  16753  strcollnft  16754  strcollnfALT  16756  sscoll2  16758  subctctexmid  16774  domomsubct  16775  exmidsbthrlem  16802  sbthom  16806  qdencn  16807  qdiff  16833  ltlenmkv  16856  gfsumval  16862