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  5372  feq1  5393  sbcfng  5408  sbcfg  5409  f1eq1  5461  foeq1  5479  f1oeq1  5495  f1oeq2  5496  f1oeq3  5497  ffoss  5539  brprcneu  5554  fv3  5584  tz6.12f  5590  ssimaex  5625  fvopab3g  5637  fvopab3ig  5638  fvopab6  5661  fmptco  5731  elunirn  5816  f1imaeq  5825  foeqcnvco  5840  fliftfun  5846  fliftval  5850  isoeq1  5851  isoeq4  5854  isoini  5868  isopolem  5872  f1oiso2  5877  riotabidv  5882  cbvriota  5891  acexmid  5924  ovanraleqv  5949  cbvoprab1  5998  cbvoprab2  5999  cbvoprab12  6000  cbvmpox  6004  ov  6046  ovig  6048  ovg  6066  caovimo  6121  caoftrn  6172  opabex3d  6187  opabex3  6188  uchoice  6204  elxp6  6236  unielxp  6241  dfoprab4  6259  dfoprab4f  6260  fmpox  6267  xporderlem  6298  poxp  6299  cnvoprab  6301  f1od2  6302  opeliunxp2f  6305  rbropapd  6309  dftpos4  6330  tpostpos  6331  smoiso  6369  tfrlem3ag  6376  tfrlem3a  6377  tfr0dm  6389  tfrlemisucaccv  6392  tfrlemiex  6398  tfrlemi1  6399  tfrlemi14d  6400  tfrexlem  6401  tfr1onlem3ag  6404  tfr1onlemsucaccv  6408  tfr1onlemex  6414  tfr1onlemaccex  6415  tfr1onlemres  6416  tfrcllemsucaccv  6421  tfrcllembxssdm  6423  tfrcllemex  6427  tfrcllemaccex  6428  tfrcllemres  6429  tfrcldm  6430  frec0g  6464  frecabcl  6466  freccllem  6469  frecfcllem  6471  frecsuclem  6473  frecsuc  6474  nnacan  6579  nnmcan  6586  nnaordex  6595  ertr  6616  brecop  6693  eroveu  6694  ecopovtrn  6700  ecopovtrng  6703  th3qlem1  6705  th3qlem2  6706  th3q  6708  elpm2r  6734  mapsncnv  6763  elixp2  6770  ixpeq1  6777  elixpsn  6803  ixpsnf1o  6804  mapsnen  6879  map1  6880  xpsnen  6889  endisj  6892  pw2f1odclem  6904  xpf1o  6914  phplem3g  6926  ssfiexmid  6946  domfiexmid  6948  findcard2s  6960  isinfinf  6967  ac6sfi  6968  fiintim  7001  fisseneq  7004  opabfi  7008  f1dmvrnfibi  7019  sbthlem2  7033  isbth  7042  supeq1  7061  supeq3  7065  supeq123d  7066  supmoti  7068  eqsupti  7071  supsnti  7080  isotilem  7081  isoti  7082  supisolem  7083  supisoex  7084  cnvinfex  7093  cnvti  7094  eqinfti  7095  infvalti  7097  updjud  7157  ctssexmid  7225  omniwomnimkv  7242  exmidfodomrlemr  7281  exmidfodomrlemrALT  7282  acneq  7285  acfun  7290  tapeq1  7335  tapeq2  7336  exmidapne  7343  ccfunen  7347  cc2lem  7349  cc3  7351  ltsopi  7404  recexnq  7474  recmulnqg  7475  ltsonq  7482  lt2addnq  7488  lt2mulnq  7489  ltbtwnnqq  7499  prarloclemarch2  7503  enq0sym  7516  enq0ref  7517  enq0tr  7518  enq0breq  7520  addnq0mo  7531  mulnq0mo  7532  addnnnq0  7533  mulnnnq0  7534  nqnq0a  7538  nqnq0m  7539  elinp  7558  prcdnql  7568  prcunqu  7569  prltlu  7571  prdisj  7576  prarloclemlo  7578  prarloclem3  7581  prarloclem5  7584  ltdfpr  7590  genprndl  7605  genprndu  7606  genpdisj  7607  appdivnq  7647  ltpopr  7679  ltexprlemdisj  7690  ltexprlemloc  7691  ltexprlemrl  7694  ltexprlemru  7696  ltexpri  7697  recexprlemm  7708  recexprlemdisj  7714  recexprlemloc  7715  recexprlem1ssl  7717  recexprlem1ssu  7718  recexpr  7722  aptiprleml  7723  archpr  7727  cauappcvgprlemladdru  7740  cauappcvgprlemladdrl  7741  cauappcvgprlem1  7743  cauappcvgprlemlim  7745  cauappcvgpr  7746  caucvgprlemnkj  7750  caucvgprlemnbj  7751  caucvgprlemcl  7760  caucvgpr  7766  caucvgprprlemcbv  7771  caucvgprprlemval  7772  caucvgprprlemopu  7783  caucvgprpr  7796  suplocexpr  7809  addsrmo  7827  mulsrmo  7828  addsrpr  7829  mulsrpr  7830  lttrsr  7846  recexgt0sr  7857  caucvgsrlemcau  7877  caucvgsrlemgt1  7879  caucvgsrlemoffcau  7882  caucvgsrlemoffres  7884  caucvgsr  7886  suplocsrlem  7892  ltresr  7923  pitonn  7932  peano1nnnn  7936  peano2nnnn  7937  axprecex  7964  axcnre  7965  axpre-lttrn  7968  peano5nnnn  7976  axcaucvglemcau  7982  axcaucvglemres  7983  axpre-suploclemres  7985  axpre-suploc  7986  axlttrn  8112  axsuploc  8116  letri3  8124  letr  8126  le2add  8488  lt2add  8489  ltleadd  8490  lt2sub  8504  le2sub  8505  apreap  8631  apreim  8647  apti  8666  msq11  8946  dfinfre  9000  sup3exmid  9001  cju  9005  peano5nni  9010  1nn  9018  peano2nn  9019  nn2ge  9040  nominpos  9246  elz2  9414  dfuzi  9453  uzind  9454  supinfneg  9686  infsupneg  9687  elpqb  9741  xrletri3  9896  xrletr  9900  z2ge  9918  elixx1  9989  elioo2  10013  iooshf  10044  iooneg  10080  iccneg  10081  icoshft  10082  elfz1  10105  fzdifsuc  10173  fzrev  10176  1fv  10231  zsupcllemstep  10336  infssuzex  10340  nninfdcex  10344  zsupssdc  10345  exbtwnzlemstep  10354  exbtwnzlemshrink  10355  exbtwnzlemex  10356  exbtwnz  10357  rebtwn2zlemstep  10359  rebtwn2zlemshrink  10360  rebtwn2z  10361  qbtwnre  10363  qbtwnxr  10364  flval  10379  flqlelt  10383  flqbi  10397  flqbi2  10398  modqid2  10460  q2submod  10494  seqf1og  10630  nnesq  10768  hashunlem  10913  zfz1isolem1  10949  zfz1iso  10950  seq3coll  10951  shftlem  10998  shftfibg  11002  shftfib  11005  shftfn  11006  2shfti  11013  cjval  11027  cjth  11028  remim  11042  caucvgrelemcau  11162  caucvgre  11163  cvg1nlemcau  11166  cvg1nlemres  11167  rexanuz2  11173  recvguniq  11177  resqrexlemgt0  11202  resqrexlemoverl  11203  resqrexlemglsq  11204  resqrexlemsqa  11206  resqrexlemex  11207  rsqrmo  11209  resqrtcl  11211  rersqrtthlem  11212  absdiflt  11274  absdifle  11275  cau3lem  11296  icodiamlt  11362  maxleast  11395  negfi  11410  minmax  11412  lemininf  11416  ltmininf  11417  xrmaxlesup  11441  xrminmax  11447  xrltmininf  11452  xrlemininf  11453  iooinsup  11459  clim  11463  clim2  11465  climshftlemg  11484  addcn2  11492  climcau  11529  summodc  11565  fsum3  11569  fsum2dlemstep  11616  fisumcom2  11620  fsum00  11644  ntrivcvgap0  11731  prodeq1f  11734  prodeq2w  11738  prodeq2  11739  prodmodc  11760  zproddc  11761  fprodseq  11765  fprodntrivap  11766  fprod2dlemstep  11804  fprodcom2fi  11808  sin01bnd  11939  cos01bnd  11940  divalgmod  12109  ndvdssub  12112  gcdsupex  12149  gcdsupcl  12150  gcddvds  12155  dvdslegcd  12156  bezoutlemmain  12190  bezoutlemex  12193  bezoutlemzz  12194  bezoutlemeu  12199  bezoutlemle  12200  bezoutlemsup  12201  dfgcd3  12202  dfgcd2  12206  gcddiv  12211  lcmval  12256  lcmcllem  12260  dvdslcm  12262  lcmledvds  12263  lcmgcdlem  12270  lcmdvds  12272  coprmgcdb  12281  ncoprmgcdne1b  12282  coprmdvds1  12284  qredeu  12290  divgcdcoprm0  12294  divgcdcoprmex  12295  isprm3  12311  pw2dvdslemn  12358  pw2dvdseu  12361  oddpwdclemxy  12362  qnumdencl  12380  qnumdenbi  12385  crth  12417  reumodprminv  12447  pythagtriplem19  12476  pceu  12489  pczpre  12491  pcdiv  12496  pc11  12525  dvdsprmpweqle  12531  prmpwdvds  12549  pockthi  12552  infpnlem2  12554  elgz  12565  4sqlem12  12596  ennnfonelemim  12666  exmidunben  12668  ctinfom  12670  ctiunctlemu1st  12676  ctiunctlemu2nd  12677  ctiunctlemudc  12679  ctiunctlemfo  12681  infpn2  12698  ptex  12966  prdsval  12975  f1ocpbllem  13012  ercpbl  13033  erlecpbl  13034  grpidvalg  13075  grpidpropdg  13076  mgmlrid  13081  igsumvalx  13091  gsumfzval  13093  gsumress  13097  gsumval2  13099  issgrpd  13114  sgrppropd  13115  ismnddef  13120  sgrpidmndm  13122  ismndd  13139  mndpropd  13142  mndinvmod  13147  mnd1  13157  ismhm  13163  mhmex  13164  mhmpropd  13168  issubm  13174  insubm  13187  grppropd  13219  dfgrp2  13229  isgrpid2  13242  isgrpinv  13256  grplrinv  13259  grpidinv2  13260  grpidinv  13261  dfgrp3mlem  13300  grplactcnv  13304  releqgg  13426  eqgex  13427  eqgfval  13428  eqgval  13429  isghm  13449  ghmrn  13463  resghm  13466  ghmpropd  13489  cmnpropd  13501  ablpropd  13502  imasabl  13542  isrng  13566  rngdi  13572  rngdir  13573  rngpropd  13587  dfur2g  13594  issrg  13597  srgideu  13604  srgidmlem  13610  issrgid  13613  srg1zr  13619  isring  13632  ringideu  13649  ringidmlem  13654  isringid  13657  ringid  13658  ringpropd  13670  ring1  13691  oppr0g  13713  oppr1g  13714  reldvdsrsrg  13724  dvdsrvald  13725  dvdsrd  13726  dvdsrtr  13733  unitgrp  13748  dvdsrpropdg  13779  unitpropdg  13780  rhmopp  13808  opprnzrbg  13817  opprsubrngg  13843  issubrg  13853  subrg1  13863  subrgugrp  13872  resrhm2b  13881  subrgpropd  13885  rhmpropd  13886  opprdomnbg  13906  aprval  13914  aprap  13918  islmod  13923  lmodlema  13924  islmodd  13925  lmodfopnelem2  13957  lmodprop2d  13980  islssm  13989  islssmg  13990  rnglidlrng  14130  isridl  14136  df2idl2rng  14140  quscrng  14165  istopg  14319  fiinbas  14369  eltg2  14373  topbas  14387  neiint  14465  neipsm  14474  opnneissb  14475  opnssneib  14476  innei  14483  restbasg  14488  iscnp4  14538  cnpnei  14539  cnconst2  14553  cnptopresti  14558  cnptoprest  14559  cnpdis  14562  lmss  14566  lmres  14568  txbas  14578  eltx  14579  neitx  14588  txcnp  14591  txcnmpt  14593  uptx  14594  txdis  14597  txdis1cn  14598  txlm  14599  txhmeo  14639  ispsmet  14643  ismet  14664  isxmet  14665  bldisj  14721  blininf  14744  blssexps  14749  blssex  14750  ssblex  14751  xmspropd  14797  mspropd  14798  neibl  14811  metequiv  14815  bdmopn  14824  metrest  14826  xmetxp  14827  xmetxpbl  14828  xmettx  14830  metcnp3  14831  tgioo  14874  tgqioo  14875  addcncntoplem  14881  mpomulcn  14886  mulcncflem  14927  dedekindeu  14943  dedekindicclemicc  14952  limccl  14979  ellimc3apf  14980  limcimolemlt  14984  limccoap  14998  elply2  15055  sin0pilem2  15102  sincosq1sgn  15146  sincosq2sgn  15147  sincosq3sgn  15148  sincosq4sgn  15149  perfect  15321  lgsval  15329  lgsdir2lem5  15357  lgsne0  15363  lgsquadlem1  15402  lgsquadlem2  15403  lgsquadlem3  15404  lgsquad  15405  2lgslem3  15426  2sqlem8a  15447  2sqlem8  15448  2sqlem9  15449  bj-sseq  15522  bj-charfunbi  15541  bj-nalset  15625  bj-indeq  15659  bj-2inf  15668  strcoll2  15713  strcollnft  15714  strcollnfALT  15716  sscoll2  15718  subctctexmid  15731  domomsubct  15732  exmidsbthrlem  15753  sbthom  15757  qdencn  15758  ltlenmkv  15801