Theorem anbi12d 477

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 469	. 2 |- ( ph -> ( ( ps /\ th ) <-> ( ch /\ th ) ) )
3		anbi12d.2	. . 3 |- ( ph -> ( th <-> ta ) )
4	3	anbi2d 468	. 2 |- ( ph -> ( ( ch /\ th ) <-> ( ch /\ ta ) ) )
5	2, 4	bitrd 188	1 |- ( ph -> ( ( ps /\ th ) <-> ( ch /\ ta ) ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm4.38  613  pm5.17dc  916  orbididc  966  ifpbi123d  1005  3anbi123d  1353  xorbi2d  1429  xorbi1d  1430  drsb1  1852  mopick  2165  clelab  2366  cbvrmow  2735  cbvrexfw  2776  cbvrexf  2778  cbvreu  2784  cbvrexvw  2791  cbvreuvw  2792  cbvrexdva2  2794  cbvrab  2819  gencbvex  2869  rspce  2924  eqvincf  2951  ceqsrexv  2956  elrabf  2980  rexab2  2992  reu2  3014  reu6  3015  rmo4  3019  reu8  3022  reuind  3031  sbcan  3094  sbcang  3095  reu8nf  3133  sbcabel  3134  rmob  3145  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  difjust  3221  injust  3225  eldif  3229  ssconb  3362  elin  3412  opeq1  3904  opeq2  3905  2ralunsn  3924  elunii  3940  csbunig  3943  eluniab  3947  cbvopab  4203  cbvopab1  4205  cbvopab2  4206  cbvopab1s  4207  cbvopab2v  4209  cbvmptf  4227  cbvmpt  4228  trel  4238  nalset  4265  elssabg  4286  mss  4368  exss  4369  opelopab2a  4409  poeq1  4446  pocl  4450  soeq1  4462  weeq1  4503  weeq2  4504  ordeq  4519  zfun  4581  snnex  4596  reusv3  4608  ontr2exmid  4674  regexmid  4684  onintexmid  4722  reg3exmid  4729  peano5  4747  limom  4763  nnregexmid  4770  vtoclr  4825  opeliunxp  4832  poinxp  4846  opbrop  4856  csbxpg  4858  opeliunxp2  4922  relop  4932  brcogw  4951  elrnmpt1  5035  elsnres  5102  dfres2  5118  inimasn  5208  xpcanm  5230  xpcan2m  5231  elxp4  5278  elxp5  5279  cnvsom  5334  sbcfung  5404  funopg  5414  fununi  5452  funcnvuni  5453  fneq1  5472  2elresin  5497  feq1  5519  sbcfng  5534  sbcfg  5535  f1eq1  5596  foeq1  5614  f1oeq1  5630  f1oeq2  5631  f1oeq3  5632  ffoss  5675  brprcneu  5691  fv3  5721  tz6.12f  5727  ssimaex  5767  fvopab3g  5781  fvopab3ig  5782  fvopab6  5808  fmptco  5877  fsn2g  5886  funopsn  5894  funopdmsn  5898  elunirn  5975  f1imaeq  5984  foeqcnvco  5999  fliftfun  6005  fliftval  6009  isoeq1  6010  isoeq4  6013  isoini  6027  isopolem  6031  f1oiso2  6036  riotabidv  6043  cbvriotavw  6052  cbvriota  6053  acexmid  6087  ovanraleqv  6112  cbvoprab1  6163  cbvoprab2  6164  cbvoprab12  6165  cbvmpox  6169  ov  6211  ovig  6213  ovg  6231  caovimo  6286  caoftrn  6339  opabex3d  6354  opabex3  6355  uchoice  6375  elxp6  6407  unielxp  6412  dfoprab4  6430  dfoprab4f  6431  fmpox  6440  xporderlem  6471  poxp  6472  cnvoprab  6474  f1od2  6475  opeliunxp2f  6513  rbropapd  6517  dftpos4  6538  tpostpos  6539  smoiso  6577  tfrlem3ag  6584  tfrlem3a  6585  tfr0dm  6597  tfrlemisucaccv  6600  tfrlemiex  6606  tfrlemi1  6607  tfrlemi14d  6608  tfrexlem  6609  tfr1onlem3ag  6612  tfr1onlemsucaccv  6616  tfr1onlemex  6622  tfr1onlemaccex  6623  tfr1onlemres  6624  tfrcllemsucaccv  6629  tfrcllembxssdm  6631  tfrcllemex  6635  tfrcllemaccex  6636  tfrcllemres  6637  tfrcldm  6638  frec0g  6672  frecabcl  6674  freccllem  6677  frecfcllem  6679  frecsuclem  6681  frecsuc  6682  nnacan  6789  nnmcan  6796  nnaordex  6805  ertr  6826  brecop  6903  eroveu  6904  ecopovtrn  6910  ecopovtrng  6913  th3qlem1  6915  th3qlem2  6916  th3q  6918  elpm2r  6944  mapsncnv  6981  elixp2  6988  ixpeq1  6995  elixpsn  7021  ixpsnf1o  7022  mapsnend  7103  mapsnen  7104  map1  7105  xpsnen  7123  endisj  7126  pw2f1odclem  7138  xpf1o  7148  mapunen  7155  phplem3g  7161  ssfiexmid  7182  ssfiexmidt  7184  domfiexmid  7186  findcard2s  7198  isinfinf  7205  ac6sfi  7206  fiintim  7242  fisseneq  7246  opabfi  7251  f1dmvrnfibi  7262  sbthlem2  7280  isbth  7289  isfsupp  7294  supeq1  7332  supeq3  7336  supeq123d  7337  supmoti  7339  eqsupti  7342  supsnti  7351  isotilem  7352  isoti  7353  supisolem  7354  supisoex  7355  cnvinfex  7364  cnvti  7365  eqinfti  7366  infvalti  7368  updjud  7428  ctssexmid  7496  omniwomnimkv  7513  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  acneq  7564  acfun  7569  papeq1  7615  papeq2  7616  tapeq1  7624  tapeq2  7625  exmidapne  7632  ccfunen  7636  cc2lem  7638  cc3  7640  ltsopi  7693  recexnq  7763  recmulnqg  7764  ltsonq  7771  lt2addnq  7777  lt2mulnq  7778  ltbtwnnqq  7788  prarloclemarch2  7792  enq0sym  7805  enq0ref  7806  enq0tr  7807  enq0breq  7809  addnq0mo  7820  mulnq0mo  7821  addnnnq0  7822  mulnnnq0  7823  nqnq0a  7827  nqnq0m  7828  elinp  7847  prcdnql  7857  prcunqu  7858  prltlu  7860  prdisj  7865  prarloclemlo  7867  prarloclem3  7870  prarloclem5  7873  ltdfpr  7879  genprndl  7894  genprndu  7895  genpdisj  7896  appdivnq  7936  ltpopr  7968  ltexprlemdisj  7979  ltexprlemloc  7980  ltexprlemrl  7983  ltexprlemru  7985  ltexpri  7986  recexprlemm  7997  recexprlemdisj  8003  recexprlemloc  8004  recexprlem1ssl  8006  recexprlem1ssu  8007  recexpr  8011  aptiprleml  8012  archpr  8016  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  cauappcvgprlem1  8032  cauappcvgprlemlim  8034  cauappcvgpr  8035  caucvgprlemnkj  8039  caucvgprlemnbj  8040  caucvgprlemcl  8049  caucvgpr  8055  caucvgprprlemcbv  8060  caucvgprprlemval  8061  caucvgprprlemopu  8072  caucvgprpr  8085  suplocexpr  8098  addsrmo  8116  mulsrmo  8117  addsrpr  8118  mulsrpr  8119  lttrsr  8135  recexgt0sr  8146  caucvgsrlemcau  8166  caucvgsrlemgt1  8168  caucvgsrlemoffcau  8171  caucvgsrlemoffres  8173  caucvgsr  8175  suplocsrlem  8181  ltresr  8212  pitonn  8221  peano1nnnn  8225  peano2nnnn  8226  axprecex  8253  axcnre  8254  axpre-lttrn  8257  peano5nnnn  8265  axcaucvglemcau  8271  axcaucvglemres  8272  axpre-suploclemres  8274  axpre-suploc  8275  axlttrn  8400  axsuploc  8404  letri3  8412  letr  8414  le2add  8779  lt2add  8780  ltleadd  8781  lt2sub  8795  le2sub  8796  apreap  8923  apreim  8939  apti  8958  msq11  9240  dfinfre  9294  sup3exmid  9295  cju  9299  peano5nni  9316  1nn  9324  peano2nn  9325  nn2ge  9346  nominpos  9554  elz2  9727  dfuzi  9767  uzind  9768  supinfneg  10011  infsupneg  10012  elpqb  10067  xrletri3  10223  xrletr  10227  z2ge  10245  elixx1  10316  elioo2  10340  iooshf  10371  iooneg  10407  iccneg  10408  icoshft  10409  elfz1  10433  fzdifsuc  10505  fzrev  10508  1fv  10563  zsupcllemstep  10679  infssuzex  10683  nninfdcex  10689  zsupssdc  10690  exbtwnzlemstep  10699  exbtwnzlemshrink  10700  exbtwnzlemex  10701  exbtwnz  10702  rebtwn2zlemstep  10704  rebtwn2zlemshrink  10705  rebtwn2z  10706  qbtwnre  10708  qbtwnxr  10709  flval  10724  flqlelt  10729  flaplelt  10730  flqbi  10746  flqbi2  10747  modqid2  10809  q2submod  10843  seqf1og  10979  nnesq  11118  hashunlem  11266  hashfibclem  11304  hashf1lem1  11307  hashf1lem2  11308  zfz1isolem1  11314  zfz1iso  11315  seq3coll  11316  fundm2domnop0  11322  pfxsuffeqwrdeq  11492  swrdpfx  11501  wrd2ind  11517  swrdccatin2  11523  swrdccatin2d  11538  pfxccatin12d  11539  reuccatpfxs1lem  11540  reuccatpfxs1  11541  shftlem  11603  shftfibg  11607  shftfib  11610  shftfn  11611  2shfti  11618  cjval  11632  cjth  11633  remim  11647  caucvgrelemcau  11768  caucvgre  11769  cvg1nlemcau  11772  cvg1nlemres  11773  rexanuz2  11779  recvguniq  11783  resqrexlemgt0  11808  resqrexlemoverl  11809  resqrexlemglsq  11810  resqrexlemsqa  11812  resqrexlemex  11813  rsqrmo  11815  resqrtcl  11817  rersqrtthlem  11818  absdiflt  11881  absdifle  11882  cau3lem  11903  icodiamlt  11969  maxleast  12002  negfi  12017  minmax  12020  lemininf  12024  ltmininf  12025  xrmaxlesup  12050  xrminmax  12056  xrltmininf  12061  xrlemininf  12062  iooinsup  12068  clim  12072  clim2  12074  climshftlemg  12093  addcn2  12101  climcau  12138  summodc  12175  fsum3  12179  fsum2dlemstep  12226  fisumcom2  12230  fsum00  12254  ntrivcvgap0  12341  prodeq1f  12344  prodeq2w  12348  prodeq2  12349  prodmodc  12370  zproddc  12371  fprodseq  12375  fprodntrivap  12376  fprod2dlemstep  12414  fprodcom2fi  12418  sin01bnd  12549  cos01bnd  12550  divalgmod  12719  ndvdssub  12722  gcdsupex  12759  gcdsupcl  12760  gcddvds  12765  dvdslegcd  12766  bezoutlemmain  12800  bezoutlemex  12803  bezoutlemzz  12804  bezoutlemeu  12809  bezoutlemle  12810  bezoutlemsup  12811  dfgcd3  12812  dfgcd2  12816  gcddiv  12821  lcmval  12866  lcmcllem  12870  dvdslcm  12872  lcmledvds  12873  lcmgcdlem  12880  lcmdvds  12882  coprmgcdb  12891  ncoprmgcdne1b  12892  coprmdvds1  12894  qredeu  12900  divgcdcoprm0  12904  divgcdcoprmex  12905  isprm3  12921  pwbdvdslemn  12969  pwbdvdseu  12972  nnmaxpwlemxy  12973  qnumdencl  12992  qnumdenbi  12997  crth  13031  reumodprminv  13061  pythagtriplem19  13090  pceu  13103  pczpre  13105  pcdiv  13110  pc11  13139  dvdsprmpweqle  13145  prmpwdvds  13163  pockthi  13166  infpnlem2  13168  elgz  13179  4sqlem12  13210  ennnfonelemim  13373  exmidunben  13375  ctinfom  13377  ctiunctlemu1st  13383  ctiunctlemu2nd  13384  ctiunctlemudc  13386  ctiunctlemfo  13388  infpn2  13405  ptex  13677  f1ocpbllem  13690  ercpbl  13711  erlecpbl  13712  grpidvalg  13752  grpidpropdg  13753  mgmlrid  13758  gzsumvalx  13768  gzsumfzval  13770  gzsumress  13771  gzsumval2  13773  issgrpd  13786  sgrppropd  13787  ismnddef  13790  sgrpidmndm  13792  ismndd  13809  mndpropd  13812  mndinvmod  13817  mnd1  13821  ismhm  13827  mhmex  13828  mhmpropd  13832  issubm  13838  insubm  13851  grppropd  13881  dfgrp2  13891  isgrpid2  13904  isgrpinv  13918  grplrinv  13921  grpidinv2  13922  grpidinv  13923  dfgrp3mlem  13962  grplactcnv  13966  releqgg  14082  eqgex  14083  eqgfval  14084  eqgval  14085  isghm  14105  ghmrn  14119  resghm  14122  ghmpropd  14145  resscntz  14166  cmnpropd  14188  ablpropd  14189  imasabl  14230  gsumvalfi  14242  prdsval  14280  isrng  14340  rngdi  14346  rngdir  14347  rngpropd  14361  rng1zrlem  14365  dfur2g  14373  issrg  14376  srgideu  14383  srgidmlem  14389  issrgid  14392  isring  14411  ringideu  14428  ringidmlem  14434  isringid  14437  ringid  14438  ringpropd  14450  ring1  14471  oppr0g  14496  oppr1g  14497  dvdsrvald  14509  dvdsrd  14510  dvdsrtr  14517  unitgrp  14532  dvdsrpropdg  14563  unitpropdg  14564  rhmopp  14592  opprnzrbg  14601  opprlring  14613  opprsubrngg  14628  issubrg  14638  subrg1  14648  subrgugrp  14657  resrhm2b  14666  subrgpropd  14670  rhmpropd  14671  opprdomnbg  14692  aprval  14700  aprap  14707  aprprop  14710  opprdrng  14729  islmod  14736  lmodlema  14737  islmodd  14738  lmodfopnelem2  14771  lmodprop2d  14794  islssm  14803  islssmg  14804  rnglidlrng  14944  isridl  14950  df2idl2rng  14954  quscrng  14979  isassa  15111  assalem  15112  isassad  15120  assapropd  15123  istopg  15225  fiinbas  15275  eltg2  15279  topbas  15293  neiint  15371  neipsm  15380  opnneissb  15381  opnssneib  15382  innei  15389  restbasg  15394  iscnp4  15444  cnpnei  15445  cnconst2  15459  cnptopresti  15464  cnptoprest  15465  cnpdis  15468  lmss  15472  lmres  15474  txbas  15484  eltx  15485  neitx  15494  txcnp  15497  txcnmpt  15499  uptx  15500  txdis  15503  txdis1cn  15504  txlm  15505  txhmeo  15545  ispsmet  15549  ismet  15570  isxmet  15571  bldisj  15627  blininf  15650  blssexps  15655  blssex  15656  ssblex  15657  xmspropd  15703  mspropd  15704  neibl  15717  metequiv  15721  bdmopn  15730  metrest  15732  xmetxp  15733  xmetxpbl  15734  xmettx  15736  metcnp3  15737  tgioo  15780  tgqioo  15781  addcncntoplem  15787  mpomulcn  15792  mulcncflem  15833  dedekindeu  15849  dedekindicclemicc  15858  limccl  15885  ellimc3apf  15886  limcimolemlt  15890  limccoap  15904  elply2  15961  sin0pilem2  16009  sincosq1sgn  16053  sincosq2sgn  16054  sincosq3sgn  16055  sincosq4sgn  16056  zprmlogbaplem3  16217  zprmlogbap  16218  pellexlem3  16231  perfect  16301  prmefexple  16308  bpos1lem  16309  bposlem1  16311  bposlem9  16319  lgsval  16328  lgsdir2lem5  16356  lgsne0  16362  lgsquadlem1  16401  lgsquadlem2  16402  lgsquadlem3  16403  lgsquad  16404  2lgslem3  16425  2sqlem8a  16446  2sqlem8  16447  2sqlem9  16448  gropd  16493  grstructd2dom  16494  incistruhgr  16536  uhgr2edg  16652  vtxd0nedgbfi  16745  wlkeq  16800  istrl  16831  clwwlkn2  16867  eupthsg  16891  iseupth  16893  eupth2lem1  16904  depind  16955  bj-sseq  17025  bj-charfunbi  17042  bj-nalset  17126  bj-indeq  17160  bj-2inf  17169  strcoll2  17214  strcollnft  17215  strcollnfALT  17217  sscoll2  17219  subctctexmid  17235  domomsubct  17236  exmidsbthrlem  17273  sbthom  17277  qdencn  17278  qdiff  17305  ltlenmkv  17327  alsbid  17350