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  2161  clelab  2362  cbvrmow  2729  cbvrexfw  2770  cbvrexf  2772  cbvreu  2778  cbvrexvw  2785  cbvreuvw  2786  cbvrexdva2  2788  cbvrab  2813  gencbvex  2863  rspce  2918  eqvincf  2945  ceqsrexv  2950  elrabf  2974  rexab2  2986  reu2  3008  reu6  3009  rmo4  3013  reu8  3016  reuind  3025  sbcan  3088  sbcang  3089  reu8nf  3127  sbcabel  3128  rmob  3139  cbvrexcsf  3205  cbvreucsf  3206  cbvrabcsf  3207  difjust  3215  injust  3219  eldif  3223  ssconb  3356  elin  3406  opeq1  3888  opeq2  3889  2ralunsn  3908  elunii  3924  csbunig  3927  eluniab  3931  cbvopab  4186  cbvopab1  4188  cbvopab2  4189  cbvopab1s  4190  cbvopab2v  4192  cbvmptf  4209  cbvmpt  4210  trel  4220  nalset  4245  elssabg  4265  mss  4347  exss  4348  opelopab2a  4388  poeq1  4425  pocl  4429  soeq1  4441  weeq1  4482  weeq2  4483  ordeq  4498  zfun  4560  snnex  4574  reusv3  4586  ontr2exmid  4652  regexmid  4662  onintexmid  4700  reg3exmid  4707  peano5  4725  limom  4741  nnregexmid  4748  vtoclr  4803  opeliunxp  4810  poinxp  4824  opbrop  4834  csbxpg  4836  opeliunxp2  4900  relop  4910  brcogw  4929  elrnmpt1  5013  elsnres  5080  dfres2  5095  inimasn  5185  xpcanm  5207  xpcan2m  5208  elxp4  5255  elxp5  5256  cnvsom  5311  sbcfung  5381  funopg  5391  fununi  5429  funcnvuni  5430  fneq1  5449  2elresin  5474  feq1  5496  sbcfng  5511  sbcfg  5512  f1eq1  5573  foeq1  5591  f1oeq1  5607  f1oeq2  5608  f1oeq3  5609  ffoss  5652  brprcneu  5668  fv3  5698  tz6.12f  5704  ssimaex  5743  fvopab3g  5755  fvopab3ig  5756  fvopab6  5779  fmptco  5848  fsn2g  5857  funopsn  5865  funopdmsn  5869  elunirn  5945  f1imaeq  5954  foeqcnvco  5969  fliftfun  5975  fliftval  5979  isoeq1  5980  isoeq4  5983  isoini  5997  isopolem  6001  f1oiso2  6006  riotabidv  6013  cbvriotavw  6022  cbvriota  6023  acexmid  6057  ovanraleqv  6082  cbvoprab1  6133  cbvoprab2  6134  cbvoprab12  6135  cbvmpox  6139  ov  6181  ovig  6183  ovg  6201  caovimo  6256  caoftrn  6308  opabex3d  6323  opabex3  6324  uchoice  6344  elxp6  6376  unielxp  6381  dfoprab4  6399  dfoprab4f  6400  fmpox  6409  xporderlem  6440  poxp  6441  cnvoprab  6443  f1od2  6444  opeliunxp2f  6482  rbropapd  6486  dftpos4  6507  tpostpos  6508  smoiso  6546  tfrlem3ag  6553  tfrlem3a  6554  tfr0dm  6566  tfrlemisucaccv  6569  tfrlemiex  6575  tfrlemi1  6576  tfrlemi14d  6577  tfrexlem  6578  tfr1onlem3ag  6581  tfr1onlemsucaccv  6585  tfr1onlemex  6591  tfr1onlemaccex  6592  tfr1onlemres  6593  tfrcllemsucaccv  6598  tfrcllembxssdm  6600  tfrcllemex  6604  tfrcllemaccex  6605  tfrcllemres  6606  tfrcldm  6607  frec0g  6641  frecabcl  6643  freccllem  6646  frecfcllem  6648  frecsuclem  6650  frecsuc  6651  nnacan  6758  nnmcan  6765  nnaordex  6774  ertr  6795  brecop  6872  eroveu  6873  ecopovtrn  6879  ecopovtrng  6882  th3qlem1  6884  th3qlem2  6885  th3q  6887  elpm2r  6913  mapsncnv  6943  elixp2  6950  ixpeq1  6957  elixpsn  6983  ixpsnf1o  6984  mapsnend  7065  mapsnen  7066  map1  7067  xpsnen  7085  endisj  7088  pw2f1odclem  7100  xpf1o  7110  mapunen  7117  phplem3g  7123  ssfiexmid  7144  ssfiexmidt  7146  domfiexmid  7148  findcard2s  7160  isinfinf  7167  ac6sfi  7168  fiintim  7204  fisseneq  7208  opabfi  7213  f1dmvrnfibi  7224  sbthlem2  7241  isbth  7250  isfsupp  7255  supeq1  7290  supeq3  7294  supeq123d  7295  supmoti  7297  eqsupti  7300  supsnti  7309  isotilem  7310  isoti  7311  supisolem  7312  supisoex  7313  cnvinfex  7322  cnvti  7323  eqinfti  7324  infvalti  7326  updjud  7386  ctssexmid  7454  omniwomnimkv  7471  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  acneq  7522  acfun  7527  papeq1  7573  papeq2  7574  tapeq1  7582  tapeq2  7583  exmidapne  7590  ccfunen  7594  cc2lem  7596  cc3  7598  ltsopi  7651  recexnq  7721  recmulnqg  7722  ltsonq  7729  lt2addnq  7735  lt2mulnq  7736  ltbtwnnqq  7746  prarloclemarch2  7750  enq0sym  7763  enq0ref  7764  enq0tr  7765  enq0breq  7767  addnq0mo  7778  mulnq0mo  7779  addnnnq0  7780  mulnnnq0  7781  nqnq0a  7785  nqnq0m  7786  elinp  7805  prcdnql  7815  prcunqu  7816  prltlu  7818  prdisj  7823  prarloclemlo  7825  prarloclem3  7828  prarloclem5  7831  ltdfpr  7837  genprndl  7852  genprndu  7853  genpdisj  7854  appdivnq  7894  ltpopr  7926  ltexprlemdisj  7937  ltexprlemloc  7938  ltexprlemrl  7941  ltexprlemru  7943  ltexpri  7944  recexprlemm  7955  recexprlemdisj  7961  recexprlemloc  7962  recexprlem1ssl  7964  recexprlem1ssu  7965  recexpr  7969  aptiprleml  7970  archpr  7974  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  cauappcvgprlem1  7990  cauappcvgprlemlim  7992  cauappcvgpr  7993  caucvgprlemnkj  7997  caucvgprlemnbj  7998  caucvgprlemcl  8007  caucvgpr  8013  caucvgprprlemcbv  8018  caucvgprprlemval  8019  caucvgprprlemopu  8030  caucvgprpr  8043  suplocexpr  8056  addsrmo  8074  mulsrmo  8075  addsrpr  8076  mulsrpr  8077  lttrsr  8093  recexgt0sr  8104  caucvgsrlemcau  8124  caucvgsrlemgt1  8126  caucvgsrlemoffcau  8129  caucvgsrlemoffres  8131  caucvgsr  8133  suplocsrlem  8139  ltresr  8170  pitonn  8179  peano1nnnn  8183  peano2nnnn  8184  axprecex  8211  axcnre  8212  axpre-lttrn  8215  peano5nnnn  8223  axcaucvglemcau  8229  axcaucvglemres  8230  axpre-suploclemres  8232  axpre-suploc  8233  axlttrn  8358  axsuploc  8362  letri3  8370  letr  8372  le2add  8735  lt2add  8736  ltleadd  8737  lt2sub  8751  le2sub  8752  apreap  8878  apreim  8894  apti  8913  msq11  9193  dfinfre  9247  sup3exmid  9248  cju  9252  peano5nni  9257  1nn  9265  peano2nn  9266  nn2ge  9287  nominpos  9493  elz2  9666  dfuzi  9706  uzind  9707  supinfneg  9945  infsupneg  9946  elpqb  10000  xrletri3  10156  xrletr  10160  z2ge  10178  elixx1  10249  elioo2  10273  iooshf  10304  iooneg  10340  iccneg  10341  icoshft  10342  elfz1  10366  fzdifsuc  10437  fzrev  10440  1fv  10495  zsupcllemstep  10611  infssuzex  10615  nninfdcex  10621  zsupssdc  10622  exbtwnzlemstep  10631  exbtwnzlemshrink  10632  exbtwnzlemex  10633  exbtwnz  10634  rebtwn2zlemstep  10636  rebtwn2zlemshrink  10637  rebtwn2z  10638  qbtwnre  10640  qbtwnxr  10641  flval  10656  flqlelt  10660  flqbi  10674  flqbi2  10675  modqid2  10737  q2submod  10771  seqf1og  10907  nnesq  11046  hashunlem  11193  hashfibclem  11231  zfz1isolem1  11237  zfz1iso  11238  seq3coll  11239  fundm2domnop0  11245  pfxsuffeqwrdeq  11415  swrdpfx  11424  wrd2ind  11440  swrdccatin2  11446  swrdccatin2d  11461  pfxccatin12d  11462  reuccatpfxs1lem  11463  reuccatpfxs1  11464  shftlem  11526  shftfibg  11530  shftfib  11533  shftfn  11534  2shfti  11541  cjval  11555  cjth  11556  remim  11570  caucvgrelemcau  11690  caucvgre  11691  cvg1nlemcau  11694  cvg1nlemres  11695  rexanuz2  11701  recvguniq  11705  resqrexlemgt0  11730  resqrexlemoverl  11731  resqrexlemglsq  11732  resqrexlemsqa  11734  resqrexlemex  11735  rsqrmo  11737  resqrtcl  11739  rersqrtthlem  11740  absdiflt  11802  absdifle  11803  cau3lem  11824  icodiamlt  11890  maxleast  11923  negfi  11938  minmax  11940  lemininf  11944  ltmininf  11945  xrmaxlesup  11969  xrminmax  11975  xrltmininf  11980  xrlemininf  11981  iooinsup  11987  clim  11991  clim2  11993  climshftlemg  12012  addcn2  12020  climcau  12057  summodc  12094  fsum3  12098  fsum2dlemstep  12145  fisumcom2  12149  fsum00  12173  ntrivcvgap0  12260  prodeq1f  12263  prodeq2w  12267  prodeq2  12268  prodmodc  12289  zproddc  12290  fprodseq  12294  fprodntrivap  12295  fprod2dlemstep  12333  fprodcom2fi  12337  sin01bnd  12468  cos01bnd  12469  divalgmod  12638  ndvdssub  12641  gcdsupex  12678  gcdsupcl  12679  gcddvds  12684  dvdslegcd  12685  bezoutlemmain  12719  bezoutlemex  12722  bezoutlemzz  12723  bezoutlemeu  12728  bezoutlemle  12729  bezoutlemsup  12730  dfgcd3  12731  dfgcd2  12735  gcddiv  12740  lcmval  12785  lcmcllem  12789  dvdslcm  12791  lcmledvds  12792  lcmgcdlem  12799  lcmdvds  12801  coprmgcdb  12810  ncoprmgcdne1b  12811  coprmdvds1  12813  qredeu  12819  divgcdcoprm0  12823  divgcdcoprmex  12824  isprm3  12840  pw2dvdslemn  12887  pw2dvdseu  12890  oddpwdclemxy  12891  qnumdencl  12909  qnumdenbi  12914  crth  12946  reumodprminv  12976  pythagtriplem19  13005  pceu  13018  pczpre  13020  pcdiv  13025  pc11  13054  dvdsprmpweqle  13060  prmpwdvds  13078  pockthi  13081  infpnlem2  13083  elgz  13094  4sqlem12  13125  ennnfonelemim  13259  exmidunben  13261  ctinfom  13263  ctiunctlemu1st  13269  ctiunctlemu2nd  13270  ctiunctlemudc  13272  ctiunctlemfo  13274  infpn2  13291  ptex  13561  f1ocpbllem  13574  ercpbl  13595  erlecpbl  13596  grpidvalg  13636  grpidpropdg  13637  mgmlrid  13642  igsumvalx  13652  gsumfzval  13654  gsumress  13658  gsumval2  13660  issgrpd  13675  sgrppropd  13676  ismnddef  13679  sgrpidmndm  13681  ismndd  13698  mndpropd  13701  mndinvmod  13706  mnd1  13710  ismhm  13716  mhmex  13717  mhmpropd  13721  issubm  13727  insubm  13740  grppropd  13772  dfgrp2  13782  isgrpid2  13795  isgrpinv  13809  grplrinv  13812  grpidinv2  13813  grpidinv  13814  dfgrp3mlem  13853  grplactcnv  13857  releqgg  13973  eqgex  13974  eqgfval  13975  eqgval  13976  isghm  13996  ghmrn  14010  resghm  14013  ghmpropd  14036  cmnpropd  14048  ablpropd  14049  imasabl  14089  gfsumval  14102  prdsval  14115  isrng  14173  rngdi  14179  rngdir  14180  rngpropd  14194  rng1zrlem  14198  dfur2g  14205  issrg  14208  srgideu  14215  srgidmlem  14221  issrgid  14224  isring  14243  ringideu  14260  ringidmlem  14265  isringid  14268  ringid  14269  ringpropd  14281  ring1  14302  oppr0g  14325  oppr1g  14326  dvdsrvald  14338  dvdsrd  14339  dvdsrtr  14346  unitgrp  14361  dvdsrpropdg  14392  unitpropdg  14393  rhmopp  14421  opprnzrbg  14430  opprlring  14442  opprsubrngg  14457  issubrg  14467  subrg1  14477  subrgugrp  14486  resrhm2b  14495  subrgpropd  14499  rhmpropd  14500  opprdomnbg  14521  aprval  14529  aprap  14536  aprprop  14539  opprdrng  14558  islmod  14565  lmodlema  14566  islmodd  14567  lmodfopnelem2  14599  lmodprop2d  14622  islssm  14631  islssmg  14632  rnglidlrng  14772  isridl  14778  df2idl2rng  14782  quscrng  14807  istopg  14990  fiinbas  15040  eltg2  15044  topbas  15058  neiint  15136  neipsm  15145  opnneissb  15146  opnssneib  15147  innei  15154  restbasg  15159  iscnp4  15209  cnpnei  15210  cnconst2  15224  cnptopresti  15229  cnptoprest  15230  cnpdis  15233  lmss  15237  lmres  15239  txbas  15249  eltx  15250  neitx  15259  txcnp  15262  txcnmpt  15264  uptx  15265  txdis  15268  txdis1cn  15269  txlm  15270  txhmeo  15310  ispsmet  15314  ismet  15335  isxmet  15336  bldisj  15392  blininf  15415  blssexps  15420  blssex  15421  ssblex  15422  xmspropd  15468  mspropd  15469  neibl  15482  metequiv  15486  bdmopn  15495  metrest  15497  xmetxp  15498  xmetxpbl  15499  xmettx  15501  metcnp3  15502  tgioo  15545  tgqioo  15546  addcncntoplem  15552  mpomulcn  15557  mulcncflem  15598  dedekindeu  15614  dedekindicclemicc  15623  limccl  15650  ellimc3apf  15651  limcimolemlt  15655  limccoap  15669  elply2  15726  sin0pilem2  15773  sincosq1sgn  15817  sincosq2sgn  15818  sincosq3sgn  15819  sincosq4sgn  15820  pellexlem3  15973  perfect  15995  lgsval  16003  lgsdir2lem5  16031  lgsne0  16037  lgsquadlem1  16076  lgsquadlem2  16077  lgsquadlem3  16078  lgsquad  16079  2lgslem3  16100  2sqlem8a  16121  2sqlem8  16122  2sqlem9  16123  gropd  16168  grstructd2dom  16169  incistruhgr  16211  uhgr2edg  16327  vtxd0nedgbfi  16420  wlkeq  16475  istrl  16506  clwwlkn2  16542  eupthsg  16566  iseupth  16568  eupth2lem1  16579  depind  16630  bj-sseq  16690  bj-charfunbi  16707  bj-nalset  16791  bj-indeq  16825  bj-2inf  16834  strcoll2  16879  strcollnft  16880  strcollnfALT  16882  sscoll2  16884  subctctexmid  16900  domomsubct  16901  exmidsbthrlem  16928  sbthom  16932  qdencn  16933  qdiff  16959  ltlenmkv  16982