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  911  orbididc  961  ifpbi123d  1000  3anbi123d  1348  xorbi2d  1424  xorbi1d  1425  drsb1  1847  mopick  2158  clelab  2357  cbvrmow  2716  cbvrexfw  2757  cbvrexf  2759  cbvreu  2765  cbvrexvw  2772  cbvreuvw  2773  cbvrexdva2  2775  cbvrab  2800  gencbvex  2850  rspce  2905  eqvincf  2931  ceqsrexv  2936  elrabf  2960  rexab2  2972  reu2  2994  reu6  2995  rmo4  2999  reu8  3002  reuind  3011  sbcan  3074  sbcang  3075  reu8nf  3113  sbcabel  3114  rmob  3125  cbvrexcsf  3191  cbvreucsf  3192  cbvrabcsf  3193  difjust  3201  injust  3205  eldif  3209  ssconb  3340  elin  3390  opeq1  3862  opeq2  3863  2ralunsn  3882  elunii  3898  csbunig  3901  eluniab  3905  cbvopab  4160  cbvopab1  4162  cbvopab2  4163  cbvopab1s  4164  cbvopab2v  4166  cbvmptf  4183  cbvmpt  4184  trel  4194  nalset  4219  elssabg  4238  mss  4318  exss  4319  opelopab2a  4359  poeq1  4396  pocl  4400  soeq1  4412  weeq1  4453  weeq2  4454  ordeq  4469  zfun  4531  snnex  4545  reusv3  4557  ontr2exmid  4623  regexmid  4633  onintexmid  4671  reg3exmid  4678  peano5  4696  limom  4712  nnregexmid  4719  vtoclr  4774  opeliunxp  4781  poinxp  4795  opbrop  4805  csbxpg  4807  opeliunxp2  4870  relop  4880  brcogw  4899  elrnmpt1  4983  elsnres  5050  dfres2  5065  inimasn  5154  xpcanm  5176  xpcan2m  5177  elxp4  5224  elxp5  5225  cnvsom  5280  sbcfung  5350  funopg  5360  fununi  5398  funcnvuni  5399  fneq1  5418  2elresin  5443  feq1  5465  sbcfng  5480  sbcfg  5481  f1eq1  5537  foeq1  5555  f1oeq1  5571  f1oeq2  5572  f1oeq3  5573  ffoss  5616  brprcneu  5632  fv3  5662  tz6.12f  5668  ssimaex  5707  fvopab3g  5719  fvopab3ig  5720  fvopab6  5743  fmptco  5813  fsn2g  5822  funopsn  5830  funopdmsn  5834  elunirn  5907  f1imaeq  5916  foeqcnvco  5931  fliftfun  5937  fliftval  5941  isoeq1  5942  isoeq4  5945  isoini  5959  isopolem  5963  f1oiso2  5968  riotabidv  5973  cbvriotavw  5982  cbvriota  5983  acexmid  6017  ovanraleqv  6042  cbvoprab1  6093  cbvoprab2  6094  cbvoprab12  6095  cbvmpox  6099  ov  6141  ovig  6143  ovg  6161  caovimo  6216  caoftrn  6268  opabex3d  6283  opabex3  6284  uchoice  6300  elxp6  6332  unielxp  6337  dfoprab4  6355  dfoprab4f  6356  fmpox  6365  xporderlem  6396  poxp  6397  cnvoprab  6399  f1od2  6400  opeliunxp2f  6404  rbropapd  6408  dftpos4  6429  tpostpos  6430  smoiso  6468  tfrlem3ag  6475  tfrlem3a  6476  tfr0dm  6488  tfrlemisucaccv  6491  tfrlemiex  6497  tfrlemi1  6498  tfrlemi14d  6499  tfrexlem  6500  tfr1onlem3ag  6503  tfr1onlemsucaccv  6507  tfr1onlemex  6513  tfr1onlemaccex  6514  tfr1onlemres  6515  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  tfrcllemex  6526  tfrcllemaccex  6527  tfrcllemres  6528  tfrcldm  6529  frec0g  6563  frecabcl  6565  freccllem  6568  frecfcllem  6570  frecsuclem  6572  frecsuc  6573  nnacan  6680  nnmcan  6687  nnaordex  6696  ertr  6717  brecop  6794  eroveu  6795  ecopovtrn  6801  ecopovtrng  6804  th3qlem1  6806  th3qlem2  6807  th3q  6809  elpm2r  6835  mapsncnv  6864  elixp2  6871  ixpeq1  6878  elixpsn  6904  ixpsnf1o  6905  mapsnen  6986  map1  6987  xpsnen  7005  endisj  7008  pw2f1odclem  7020  xpf1o  7030  phplem3g  7042  ssfiexmid  7063  ssfiexmidt  7065  domfiexmid  7067  findcard2s  7079  isinfinf  7086  ac6sfi  7087  fiintim  7123  fisseneq  7127  opabfi  7132  f1dmvrnfibi  7143  sbthlem2  7157  isbth  7166  supeq1  7185  supeq3  7189  supeq123d  7190  supmoti  7192  eqsupti  7195  supsnti  7204  isotilem  7205  isoti  7206  supisolem  7207  supisoex  7208  cnvinfex  7217  cnvti  7218  eqinfti  7219  infvalti  7221  updjud  7281  ctssexmid  7349  omniwomnimkv  7366  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  acneq  7417  acfun  7422  tapeq1  7471  tapeq2  7472  exmidapne  7479  ccfunen  7483  cc2lem  7485  cc3  7487  ltsopi  7540  recexnq  7610  recmulnqg  7611  ltsonq  7618  lt2addnq  7624  lt2mulnq  7625  ltbtwnnqq  7635  prarloclemarch2  7639  enq0sym  7652  enq0ref  7653  enq0tr  7654  enq0breq  7656  addnq0mo  7667  mulnq0mo  7668  addnnnq0  7669  mulnnnq0  7670  nqnq0a  7674  nqnq0m  7675  elinp  7694  prcdnql  7704  prcunqu  7705  prltlu  7707  prdisj  7712  prarloclemlo  7714  prarloclem3  7717  prarloclem5  7720  ltdfpr  7726  genprndl  7741  genprndu  7742  genpdisj  7743  appdivnq  7783  ltpopr  7815  ltexprlemdisj  7826  ltexprlemloc  7827  ltexprlemrl  7830  ltexprlemru  7832  ltexpri  7833  recexprlemm  7844  recexprlemdisj  7850  recexprlemloc  7851  recexprlem1ssl  7853  recexprlem1ssu  7854  recexpr  7858  aptiprleml  7859  archpr  7863  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  cauappcvgprlem1  7879  cauappcvgprlemlim  7881  cauappcvgpr  7882  caucvgprlemnkj  7886  caucvgprlemnbj  7887  caucvgprlemcl  7896  caucvgpr  7902  caucvgprprlemcbv  7907  caucvgprprlemval  7908  caucvgprprlemopu  7919  caucvgprpr  7932  suplocexpr  7945  addsrmo  7963  mulsrmo  7964  addsrpr  7965  mulsrpr  7966  lttrsr  7982  recexgt0sr  7993  caucvgsrlemcau  8013  caucvgsrlemgt1  8015  caucvgsrlemoffcau  8018  caucvgsrlemoffres  8020  caucvgsr  8022  suplocsrlem  8028  ltresr  8059  pitonn  8068  peano1nnnn  8072  peano2nnnn  8073  axprecex  8100  axcnre  8101  axpre-lttrn  8104  peano5nnnn  8112  axcaucvglemcau  8118  axcaucvglemres  8119  axpre-suploclemres  8121  axpre-suploc  8122  axlttrn  8248  axsuploc  8252  letri3  8260  letr  8262  le2add  8624  lt2add  8625  ltleadd  8626  lt2sub  8640  le2sub  8641  apreap  8767  apreim  8783  apti  8802  msq11  9082  dfinfre  9136  sup3exmid  9137  cju  9141  peano5nni  9146  1nn  9154  peano2nn  9155  nn2ge  9176  nominpos  9382  elz2  9551  dfuzi  9590  uzind  9591  supinfneg  9829  infsupneg  9830  elpqb  9884  xrletri3  10039  xrletr  10043  z2ge  10061  elixx1  10132  elioo2  10156  iooshf  10187  iooneg  10223  iccneg  10224  icoshft  10225  elfz1  10248  fzdifsuc  10316  fzrev  10319  1fv  10374  zsupcllemstep  10489  infssuzex  10493  nninfdcex  10497  zsupssdc  10498  exbtwnzlemstep  10507  exbtwnzlemshrink  10508  exbtwnzlemex  10509  exbtwnz  10510  rebtwn2zlemstep  10512  rebtwn2zlemshrink  10513  rebtwn2z  10514  qbtwnre  10516  qbtwnxr  10517  flval  10532  flqlelt  10536  flqbi  10550  flqbi2  10551  modqid2  10613  q2submod  10647  seqf1og  10783  nnesq  10921  hashunlem  11067  zfz1isolem1  11104  zfz1iso  11105  seq3coll  11106  fundm2domnop0  11109  pfxsuffeqwrdeq  11279  swrdpfx  11288  wrd2ind  11304  swrdccatin2  11310  swrdccatin2d  11325  pfxccatin12d  11326  reuccatpfxs1lem  11327  reuccatpfxs1  11328  shftlem  11377  shftfibg  11381  shftfib  11384  shftfn  11385  2shfti  11392  cjval  11406  cjth  11407  remim  11421  caucvgrelemcau  11541  caucvgre  11542  cvg1nlemcau  11545  cvg1nlemres  11546  rexanuz2  11552  recvguniq  11556  resqrexlemgt0  11581  resqrexlemoverl  11582  resqrexlemglsq  11583  resqrexlemsqa  11585  resqrexlemex  11586  rsqrmo  11588  resqrtcl  11590  rersqrtthlem  11591  absdiflt  11653  absdifle  11654  cau3lem  11675  icodiamlt  11741  maxleast  11774  negfi  11789  minmax  11791  lemininf  11795  ltmininf  11796  xrmaxlesup  11820  xrminmax  11826  xrltmininf  11831  xrlemininf  11832  iooinsup  11838  clim  11842  clim2  11844  climshftlemg  11863  addcn2  11871  climcau  11908  summodc  11945  fsum3  11949  fsum2dlemstep  11996  fisumcom2  12000  fsum00  12024  ntrivcvgap0  12111  prodeq1f  12114  prodeq2w  12118  prodeq2  12119  prodmodc  12140  zproddc  12141  fprodseq  12145  fprodntrivap  12146  fprod2dlemstep  12184  fprodcom2fi  12188  sin01bnd  12319  cos01bnd  12320  divalgmod  12489  ndvdssub  12492  gcdsupex  12529  gcdsupcl  12530  gcddvds  12535  dvdslegcd  12536  bezoutlemmain  12570  bezoutlemex  12573  bezoutlemzz  12574  bezoutlemeu  12579  bezoutlemle  12580  bezoutlemsup  12581  dfgcd3  12582  dfgcd2  12586  gcddiv  12591  lcmval  12636  lcmcllem  12640  dvdslcm  12642  lcmledvds  12643  lcmgcdlem  12650  lcmdvds  12652  coprmgcdb  12661  ncoprmgcdne1b  12662  coprmdvds1  12664  qredeu  12670  divgcdcoprm0  12674  divgcdcoprmex  12675  isprm3  12691  pw2dvdslemn  12738  pw2dvdseu  12741  oddpwdclemxy  12742  qnumdencl  12760  qnumdenbi  12765  crth  12797  reumodprminv  12827  pythagtriplem19  12856  pceu  12869  pczpre  12871  pcdiv  12876  pc11  12905  dvdsprmpweqle  12911  prmpwdvds  12929  pockthi  12932  infpnlem2  12934  elgz  12945  4sqlem12  12976  ennnfonelemim  13046  exmidunben  13048  ctinfom  13050  ctiunctlemu1st  13056  ctiunctlemu2nd  13057  ctiunctlemudc  13059  ctiunctlemfo  13061  infpn2  13078  ptex  13348  prdsval  13357  f1ocpbllem  13394  ercpbl  13415  erlecpbl  13416  grpidvalg  13457  grpidpropdg  13458  mgmlrid  13463  igsumvalx  13473  gsumfzval  13475  gsumress  13479  gsumval2  13481  issgrpd  13496  sgrppropd  13497  ismnddef  13502  sgrpidmndm  13504  ismndd  13521  mndpropd  13524  mndinvmod  13529  mnd1  13539  ismhm  13545  mhmex  13546  mhmpropd  13550  issubm  13556  insubm  13569  grppropd  13601  dfgrp2  13611  isgrpid2  13624  isgrpinv  13638  grplrinv  13641  grpidinv2  13642  grpidinv  13643  dfgrp3mlem  13682  grplactcnv  13686  releqgg  13808  eqgex  13809  eqgfval  13810  eqgval  13811  isghm  13831  ghmrn  13845  resghm  13848  ghmpropd  13871  cmnpropd  13883  ablpropd  13884  imasabl  13924  isrng  13949  rngdi  13955  rngdir  13956  rngpropd  13970  dfur2g  13977  issrg  13980  srgideu  13987  srgidmlem  13993  issrgid  13996  srg1zr  14002  isring  14015  ringideu  14032  ringidmlem  14037  isringid  14040  ringid  14041  ringpropd  14053  ring1  14074  oppr0g  14096  oppr1g  14097  dvdsrvald  14109  dvdsrd  14110  dvdsrtr  14117  unitgrp  14132  dvdsrpropdg  14163  unitpropdg  14164  rhmopp  14192  opprnzrbg  14201  opprsubrngg  14227  issubrg  14237  subrg1  14247  subrgugrp  14256  resrhm2b  14265  subrgpropd  14269  rhmpropd  14270  opprdomnbg  14290  aprval  14298  aprap  14302  islmod  14307  lmodlema  14308  islmodd  14309  lmodfopnelem2  14341  lmodprop2d  14364  islssm  14373  islssmg  14374  rnglidlrng  14514  isridl  14520  df2idl2rng  14524  quscrng  14549  istopg  14725  fiinbas  14775  eltg2  14779  topbas  14793  neiint  14871  neipsm  14880  opnneissb  14881  opnssneib  14882  innei  14889  restbasg  14894  iscnp4  14944  cnpnei  14945  cnconst2  14959  cnptopresti  14964  cnptoprest  14965  cnpdis  14968  lmss  14972  lmres  14974  txbas  14984  eltx  14985  neitx  14994  txcnp  14997  txcnmpt  14999  uptx  15000  txdis  15003  txdis1cn  15004  txlm  15005  txhmeo  15045  ispsmet  15049  ismet  15070  isxmet  15071  bldisj  15127  blininf  15150  blssexps  15155  blssex  15156  ssblex  15157  xmspropd  15203  mspropd  15204  neibl  15217  metequiv  15221  bdmopn  15230  metrest  15232  xmetxp  15233  xmetxpbl  15234  xmettx  15236  metcnp3  15237  tgioo  15280  tgqioo  15281  addcncntoplem  15287  mpomulcn  15292  mulcncflem  15333  dedekindeu  15349  dedekindicclemicc  15358  limccl  15385  ellimc3apf  15386  limcimolemlt  15390  limccoap  15404  elply2  15461  sin0pilem2  15508  sincosq1sgn  15552  sincosq2sgn  15553  sincosq3sgn  15554  sincosq4sgn  15555  perfect  15727  lgsval  15735  lgsdir2lem5  15763  lgsne0  15769  lgsquadlem1  15808  lgsquadlem2  15809  lgsquadlem3  15810  lgsquad  15811  2lgslem3  15832  2sqlem8a  15853  2sqlem8  15854  2sqlem9  15855  gropd  15900  grstructd2dom  15901  incistruhgr  15943  uhgr2edg  16059  vtxd0nedgbfi  16152  wlkeq  16207  istrl  16238  clwwlkn2  16274  eupthsg  16298  iseupth  16300  eupth2lem1  16311  bj-sseq  16391  bj-charfunbi  16409  bj-nalset  16493  bj-indeq  16527  bj-2inf  16536  strcoll2  16581  strcollnft  16582  strcollnfALT  16584  sscoll2  16586  subctctexmid  16604  domomsubct  16605  exmidsbthrlem  16629  sbthom  16633  qdencn  16634  ltlenmkv  16677  gfsumval  16683