Theorem anbi12d 473

Description: Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
anbi12d.1	|- ( ph -> ( ps <-> ch ) )
anbi12d.2	|- ( ph -> ( th <-> ta ) )

Assertion

Ref	Expression
anbi12d	|- ( ph -> ( ( ps /\ th ) <-> ( ch /\ ta ) ) )

Proof of Theorem anbi12d

Step	Hyp	Ref	Expression
1		anbi12d.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	anbi1d 465	. 2 |- ( ph -> ( ( ps /\ th ) <-> ( ch /\ th ) ) )
3		anbi12d.2	. . 3 |- ( ph -> ( th <-> ta ) )
4	3	anbi2d 464	. 2 |- ( ph -> ( ( ch /\ th ) <-> ( ch /\ ta ) ) )
5	2, 4	bitrd 188	1 |- ( ph -> ( ( ps /\ th ) <-> ( ch /\ ta ) ) )

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  1847  mopick  2158  clelab  2358  cbvrmow  2717  cbvrexfw  2758  cbvrexf  2760  cbvreu  2766  cbvrexvw  2773  cbvreuvw  2774  cbvrexdva2  2776  cbvrab  2801  gencbvex  2851  rspce  2906  eqvincf  2932  ceqsrexv  2937  elrabf  2961  rexab2  2973  reu2  2995  reu6  2996  rmo4  3000  reu8  3003  reuind  3012  sbcan  3075  sbcang  3076  reu8nf  3114  sbcabel  3115  rmob  3126  cbvrexcsf  3192  cbvreucsf  3193  cbvrabcsf  3194  difjust  3202  injust  3206  eldif  3210  ssconb  3342  elin  3392  opeq1  3867  opeq2  3868  2ralunsn  3887  elunii  3903  csbunig  3906  eluniab  3910  cbvopab  4165  cbvopab1  4167  cbvopab2  4168  cbvopab1s  4169  cbvopab2v  4171  cbvmptf  4188  cbvmpt  4189  trel  4199  nalset  4224  elssabg  4243  mss  4324  exss  4325  opelopab2a  4365  poeq1  4402  pocl  4406  soeq1  4418  weeq1  4459  weeq2  4460  ordeq  4475  zfun  4537  snnex  4551  reusv3  4563  ontr2exmid  4629  regexmid  4639  onintexmid  4677  reg3exmid  4684  peano5  4702  limom  4718  nnregexmid  4725  vtoclr  4780  opeliunxp  4787  poinxp  4801  opbrop  4811  csbxpg  4813  opeliunxp2  4876  relop  4886  brcogw  4905  elrnmpt1  4989  elsnres  5056  dfres2  5071  inimasn  5161  xpcanm  5183  xpcan2m  5184  elxp4  5231  elxp5  5232  cnvsom  5287  sbcfung  5357  funopg  5367  fununi  5405  funcnvuni  5406  fneq1  5425  2elresin  5450  feq1  5472  sbcfng  5487  sbcfg  5488  f1eq1  5546  foeq1  5564  f1oeq1  5580  f1oeq2  5581  f1oeq3  5582  ffoss  5625  brprcneu  5641  fv3  5671  tz6.12f  5677  ssimaex  5716  fvopab3g  5728  fvopab3ig  5729  fvopab6  5752  fmptco  5821  fsn2g  5830  funopsn  5838  funopdmsn  5842  elunirn  5917  f1imaeq  5926  foeqcnvco  5941  fliftfun  5947  fliftval  5951  isoeq1  5952  isoeq4  5955  isoini  5969  isopolem  5973  f1oiso2  5978  riotabidv  5983  cbvriotavw  5992  cbvriota  5993  acexmid  6027  ovanraleqv  6052  cbvoprab1  6103  cbvoprab2  6104  cbvoprab12  6105  cbvmpox  6109  ov  6151  ovig  6153  ovg  6171  caovimo  6226  caoftrn  6277  opabex3d  6292  opabex3  6293  uchoice  6309  elxp6  6341  unielxp  6346  dfoprab4  6364  dfoprab4f  6365  fmpox  6374  xporderlem  6405  poxp  6406  cnvoprab  6408  f1od2  6409  opeliunxp2f  6447  rbropapd  6451  dftpos4  6472  tpostpos  6473  smoiso  6511  tfrlem3ag  6518  tfrlem3a  6519  tfr0dm  6531  tfrlemisucaccv  6534  tfrlemiex  6540  tfrlemi1  6541  tfrlemi14d  6542  tfrexlem  6543  tfr1onlem3ag  6546  tfr1onlemsucaccv  6550  tfr1onlemex  6556  tfr1onlemaccex  6557  tfr1onlemres  6558  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllemex  6569  tfrcllemaccex  6570  tfrcllemres  6571  tfrcldm  6572  frec0g  6606  frecabcl  6608  freccllem  6611  frecfcllem  6613  frecsuclem  6615  frecsuc  6616  nnacan  6723  nnmcan  6730  nnaordex  6739  ertr  6760  brecop  6837  eroveu  6838  ecopovtrn  6844  ecopovtrng  6847  th3qlem1  6849  th3qlem2  6850  th3q  6852  elpm2r  6878  mapsncnv  6907  elixp2  6914  ixpeq1  6921  elixpsn  6947  ixpsnf1o  6948  mapsnen  7029  map1  7030  xpsnen  7048  endisj  7051  pw2f1odclem  7063  xpf1o  7073  phplem3g  7085  ssfiexmid  7106  ssfiexmidt  7108  domfiexmid  7110  findcard2s  7122  isinfinf  7129  ac6sfi  7130  fiintim  7166  fisseneq  7170  opabfi  7175  f1dmvrnfibi  7186  sbthlem2  7200  isbth  7209  isfsupp  7214  supeq1  7245  supeq3  7249  supeq123d  7250  supmoti  7252  eqsupti  7255  supsnti  7264  isotilem  7265  isoti  7266  supisolem  7267  supisoex  7268  cnvinfex  7277  cnvti  7278  eqinfti  7279  infvalti  7281  updjud  7341  ctssexmid  7409  omniwomnimkv  7426  exmidfodomrlemr  7473  exmidfodomrlemrALT  7474  acneq  7477  acfun  7482  tapeq1  7531  tapeq2  7532  exmidapne  7539  ccfunen  7543  cc2lem  7545  cc3  7547  ltsopi  7600  recexnq  7670  recmulnqg  7671  ltsonq  7678  lt2addnq  7684  lt2mulnq  7685  ltbtwnnqq  7695  prarloclemarch2  7699  enq0sym  7712  enq0ref  7713  enq0tr  7714  enq0breq  7716  addnq0mo  7727  mulnq0mo  7728  addnnnq0  7729  mulnnnq0  7730  nqnq0a  7734  nqnq0m  7735  elinp  7754  prcdnql  7764  prcunqu  7765  prltlu  7767  prdisj  7772  prarloclemlo  7774  prarloclem3  7777  prarloclem5  7780  ltdfpr  7786  genprndl  7801  genprndu  7802  genpdisj  7803  appdivnq  7843  ltpopr  7875  ltexprlemdisj  7886  ltexprlemloc  7887  ltexprlemrl  7890  ltexprlemru  7892  ltexpri  7893  recexprlemm  7904  recexprlemdisj  7910  recexprlemloc  7911  recexprlem1ssl  7913  recexprlem1ssu  7914  recexpr  7918  aptiprleml  7919  archpr  7923  cauappcvgprlemladdru  7936  cauappcvgprlemladdrl  7937  cauappcvgprlem1  7939  cauappcvgprlemlim  7941  cauappcvgpr  7942  caucvgprlemnkj  7946  caucvgprlemnbj  7947  caucvgprlemcl  7956  caucvgpr  7962  caucvgprprlemcbv  7967  caucvgprprlemval  7968  caucvgprprlemopu  7979  caucvgprpr  7992  suplocexpr  8005  addsrmo  8023  mulsrmo  8024  addsrpr  8025  mulsrpr  8026  lttrsr  8042  recexgt0sr  8053  caucvgsrlemcau  8073  caucvgsrlemgt1  8075  caucvgsrlemoffcau  8078  caucvgsrlemoffres  8080  caucvgsr  8082  suplocsrlem  8088  ltresr  8119  pitonn  8128  peano1nnnn  8132  peano2nnnn  8133  axprecex  8160  axcnre  8161  axpre-lttrn  8164  peano5nnnn  8172  axcaucvglemcau  8178  axcaucvglemres  8179  axpre-suploclemres  8181  axpre-suploc  8182  axlttrn  8307  axsuploc  8311  letri3  8319  letr  8321  le2add  8683  lt2add  8684  ltleadd  8685  lt2sub  8699  le2sub  8700  apreap  8826  apreim  8842  apti  8861  msq11  9141  dfinfre  9195  sup3exmid  9196  cju  9200  peano5nni  9205  1nn  9213  peano2nn  9214  nn2ge  9235  nominpos  9441  elz2  9612  dfuzi  9651  uzind  9652  supinfneg  9890  infsupneg  9891  elpqb  9945  xrletri3  10100  xrletr  10104  z2ge  10122  elixx1  10193  elioo2  10217  iooshf  10248  iooneg  10284  iccneg  10285  icoshft  10286  elfz1  10310  fzdifsuc  10378  fzrev  10381  1fv  10436  zsupcllemstep  10552  infssuzex  10556  nninfdcex  10560  zsupssdc  10561  exbtwnzlemstep  10570  exbtwnzlemshrink  10571  exbtwnzlemex  10572  exbtwnz  10573  rebtwn2zlemstep  10575  rebtwn2zlemshrink  10576  rebtwn2z  10577  qbtwnre  10579  qbtwnxr  10580  flval  10595  flqlelt  10599  flqbi  10613  flqbi2  10614  modqid2  10676  q2submod  10710  seqf1og  10846  nnesq  10984  hashunlem  11130  zfz1isolem1  11167  zfz1iso  11168  seq3coll  11169  fundm2domnop0  11175  pfxsuffeqwrdeq  11345  swrdpfx  11354  wrd2ind  11370  swrdccatin2  11376  swrdccatin2d  11391  pfxccatin12d  11392  reuccatpfxs1lem  11393  reuccatpfxs1  11394  shftlem  11456  shftfibg  11460  shftfib  11463  shftfn  11464  2shfti  11471  cjval  11485  cjth  11486  remim  11500  caucvgrelemcau  11620  caucvgre  11621  cvg1nlemcau  11624  cvg1nlemres  11625  rexanuz2  11631  recvguniq  11635  resqrexlemgt0  11660  resqrexlemoverl  11661  resqrexlemglsq  11662  resqrexlemsqa  11664  resqrexlemex  11665  rsqrmo  11667  resqrtcl  11669  rersqrtthlem  11670  absdiflt  11732  absdifle  11733  cau3lem  11754  icodiamlt  11820  maxleast  11853  negfi  11868  minmax  11870  lemininf  11874  ltmininf  11875  xrmaxlesup  11899  xrminmax  11905  xrltmininf  11910  xrlemininf  11911  iooinsup  11917  clim  11921  clim2  11923  climshftlemg  11942  addcn2  11950  climcau  11987  summodc  12024  fsum3  12028  fsum2dlemstep  12075  fisumcom2  12079  fsum00  12103  ntrivcvgap0  12190  prodeq1f  12193  prodeq2w  12197  prodeq2  12198  prodmodc  12219  zproddc  12220  fprodseq  12224  fprodntrivap  12225  fprod2dlemstep  12263  fprodcom2fi  12267  sin01bnd  12398  cos01bnd  12399  divalgmod  12568  ndvdssub  12571  gcdsupex  12608  gcdsupcl  12609  gcddvds  12614  dvdslegcd  12615  bezoutlemmain  12649  bezoutlemex  12652  bezoutlemzz  12653  bezoutlemeu  12658  bezoutlemle  12659  bezoutlemsup  12660  dfgcd3  12661  dfgcd2  12665  gcddiv  12670  lcmval  12715  lcmcllem  12719  dvdslcm  12721  lcmledvds  12722  lcmgcdlem  12729  lcmdvds  12731  coprmgcdb  12740  ncoprmgcdne1b  12741  coprmdvds1  12743  qredeu  12749  divgcdcoprm0  12753  divgcdcoprmex  12754  isprm3  12770  pw2dvdslemn  12817  pw2dvdseu  12820  oddpwdclemxy  12821  qnumdencl  12839  qnumdenbi  12844  crth  12876  reumodprminv  12906  pythagtriplem19  12935  pceu  12948  pczpre  12950  pcdiv  12955  pc11  12984  dvdsprmpweqle  12990  prmpwdvds  13008  pockthi  13011  infpnlem2  13013  elgz  13024  4sqlem12  13055  ennnfonelemim  13125  exmidunben  13127  ctinfom  13129  ctiunctlemu1st  13135  ctiunctlemu2nd  13136  ctiunctlemudc  13138  ctiunctlemfo  13140  infpn2  13157  ptex  13427  prdsval  13436  f1ocpbllem  13473  ercpbl  13494  erlecpbl  13495  grpidvalg  13536  grpidpropdg  13537  mgmlrid  13542  igsumvalx  13552  gsumfzval  13554  gsumress  13558  gsumval2  13560  issgrpd  13575  sgrppropd  13576  ismnddef  13581  sgrpidmndm  13583  ismndd  13600  mndpropd  13603  mndinvmod  13608  mnd1  13618  ismhm  13624  mhmex  13625  mhmpropd  13629  issubm  13635  insubm  13648  grppropd  13680  dfgrp2  13690  isgrpid2  13703  isgrpinv  13717  grplrinv  13720  grpidinv2  13721  grpidinv  13722  dfgrp3mlem  13761  grplactcnv  13765  releqgg  13887  eqgex  13888  eqgfval  13889  eqgval  13890  isghm  13910  ghmrn  13924  resghm  13927  ghmpropd  13950  cmnpropd  13962  ablpropd  13963  imasabl  14003  isrng  14028  rngdi  14034  rngdir  14035  rngpropd  14049  dfur2g  14056  issrg  14059  srgideu  14066  srgidmlem  14072  issrgid  14075  srg1zr  14081  isring  14094  ringideu  14111  ringidmlem  14116  isringid  14119  ringid  14120  ringpropd  14132  ring1  14153  oppr0g  14175  oppr1g  14176  dvdsrvald  14188  dvdsrd  14189  dvdsrtr  14196  unitgrp  14211  dvdsrpropdg  14242  unitpropdg  14243  rhmopp  14271  opprnzrbg  14280  opprsubrngg  14306  issubrg  14316  subrg1  14326  subrgugrp  14335  resrhm2b  14344  subrgpropd  14348  rhmpropd  14349  opprdomnbg  14370  aprval  14378  aprap  14382  islmod  14387  lmodlema  14388  islmodd  14389  lmodfopnelem2  14421  lmodprop2d  14444  islssm  14453  islssmg  14454  rnglidlrng  14594  isridl  14600  df2idl2rng  14604  quscrng  14629  istopg  14810  fiinbas  14860  eltg2  14864  topbas  14878  neiint  14956  neipsm  14965  opnneissb  14966  opnssneib  14967  innei  14974  restbasg  14979  iscnp4  15029  cnpnei  15030  cnconst2  15044  cnptopresti  15049  cnptoprest  15050  cnpdis  15053  lmss  15057  lmres  15059  txbas  15069  eltx  15070  neitx  15079  txcnp  15082  txcnmpt  15084  uptx  15085  txdis  15088  txdis1cn  15089  txlm  15090  txhmeo  15130  ispsmet  15134  ismet  15155  isxmet  15156  bldisj  15212  blininf  15235  blssexps  15240  blssex  15241  ssblex  15242  xmspropd  15288  mspropd  15289  neibl  15302  metequiv  15306  bdmopn  15315  metrest  15317  xmetxp  15318  xmetxpbl  15319  xmettx  15321  metcnp3  15322  tgioo  15365  tgqioo  15366  addcncntoplem  15372  mpomulcn  15377  mulcncflem  15418  dedekindeu  15434  dedekindicclemicc  15443  limccl  15470  ellimc3apf  15471  limcimolemlt  15475  limccoap  15489  elply2  15546  sin0pilem2  15593  sincosq1sgn  15637  sincosq2sgn  15638  sincosq3sgn  15639  sincosq4sgn  15640  pellexlem3  15793  perfect  15815  lgsval  15823  lgsdir2lem5  15851  lgsne0  15857  lgsquadlem1  15896  lgsquadlem2  15897  lgsquadlem3  15898  lgsquad  15899  2lgslem3  15920  2sqlem8a  15941  2sqlem8  15942  2sqlem9  15943  gropd  15988  grstructd2dom  15989  incistruhgr  16031  uhgr2edg  16147  vtxd0nedgbfi  16240  wlkeq  16295  istrl  16326  clwwlkn2  16362  eupthsg  16386  iseupth  16388  eupth2lem1  16399  depind  16450  bj-sseq  16510  bj-charfunbi  16527  bj-nalset  16611  bj-indeq  16645  bj-2inf  16654  strcoll2  16699  strcollnft  16700  strcollnfALT  16702  sscoll2  16704  subctctexmid  16722  domomsubct  16723  exmidsbthrlem  16750  sbthom  16754  qdencn  16755  qdiff  16781  ltlenmkv  16803  gfsumval  16809