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  4202  cbvopab1  4204  cbvopab2  4205  cbvopab1s  4206  cbvopab2v  4208  cbvmptf  4225  cbvmpt  4226  trel  4236  nalset  4263  elssabg  4284  mss  4366  exss  4367  opelopab2a  4407  poeq1  4444  pocl  4448  soeq1  4460  weeq1  4501  weeq2  4502  ordeq  4517  zfun  4579  snnex  4594  reusv3  4606  ontr2exmid  4672  regexmid  4682  onintexmid  4720  reg3exmid  4727  peano5  4745  limom  4761  nnregexmid  4768  vtoclr  4823  opeliunxp  4830  poinxp  4844  opbrop  4854  csbxpg  4856  opeliunxp2  4920  relop  4930  brcogw  4949  elrnmpt1  5033  elsnres  5100  dfres2  5115  inimasn  5205  xpcanm  5227  xpcan2m  5228  elxp4  5275  elxp5  5276  cnvsom  5331  sbcfung  5401  funopg  5411  fununi  5449  funcnvuni  5450  fneq1  5469  2elresin  5494  feq1  5516  sbcfng  5531  sbcfg  5532  f1eq1  5593  foeq1  5611  f1oeq1  5627  f1oeq2  5628  f1oeq3  5629  ffoss  5672  brprcneu  5688  fv3  5718  tz6.12f  5724  ssimaex  5764  fvopab3g  5778  fvopab3ig  5779  fvopab6  5805  fmptco  5874  fsn2g  5883  funopsn  5891  funopdmsn  5895  elunirn  5972  f1imaeq  5981  foeqcnvco  5996  fliftfun  6002  fliftval  6006  isoeq1  6007  isoeq4  6010  isoini  6024  isopolem  6028  f1oiso2  6033  riotabidv  6040  cbvriotavw  6049  cbvriota  6050  acexmid  6084  ovanraleqv  6109  cbvoprab1  6160  cbvoprab2  6161  cbvoprab12  6162  cbvmpox  6166  ov  6208  ovig  6210  ovg  6228  caovimo  6283  caoftrn  6335  opabex3d  6350  opabex3  6351  uchoice  6371  elxp6  6403  unielxp  6408  dfoprab4  6426  dfoprab4f  6427  fmpox  6436  xporderlem  6467  poxp  6468  cnvoprab  6470  f1od2  6471  opeliunxp2f  6509  rbropapd  6513  dftpos4  6534  tpostpos  6535  smoiso  6573  tfrlem3ag  6580  tfrlem3a  6581  tfr0dm  6593  tfrlemisucaccv  6596  tfrlemiex  6602  tfrlemi1  6603  tfrlemi14d  6604  tfrexlem  6605  tfr1onlem3ag  6608  tfr1onlemsucaccv  6612  tfr1onlemex  6618  tfr1onlemaccex  6619  tfr1onlemres  6620  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllemex  6631  tfrcllemaccex  6632  tfrcllemres  6633  tfrcldm  6634  frec0g  6668  frecabcl  6670  freccllem  6673  frecfcllem  6675  frecsuclem  6677  frecsuc  6678  nnacan  6785  nnmcan  6792  nnaordex  6801  ertr  6822  brecop  6899  eroveu  6900  ecopovtrn  6906  ecopovtrng  6909  th3qlem1  6911  th3qlem2  6912  th3q  6914  elpm2r  6940  mapsncnv  6977  elixp2  6984  ixpeq1  6991  elixpsn  7017  ixpsnf1o  7018  mapsnend  7099  mapsnen  7100  map1  7101  xpsnen  7119  endisj  7122  pw2f1odclem  7134  xpf1o  7144  mapunen  7151  phplem3g  7157  ssfiexmid  7178  ssfiexmidt  7180  domfiexmid  7182  findcard2s  7194  isinfinf  7201  ac6sfi  7202  fiintim  7238  fisseneq  7242  opabfi  7247  f1dmvrnfibi  7258  sbthlem2  7275  isbth  7284  isfsupp  7289  supeq1  7326  supeq3  7330  supeq123d  7331  supmoti  7333  eqsupti  7336  supsnti  7345  isotilem  7346  isoti  7347  supisolem  7348  supisoex  7349  cnvinfex  7358  cnvti  7359  eqinfti  7360  infvalti  7362  updjud  7422  ctssexmid  7490  omniwomnimkv  7507  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  acneq  7558  acfun  7563  papeq1  7609  papeq2  7610  tapeq1  7618  tapeq2  7619  exmidapne  7626  ccfunen  7630  cc2lem  7632  cc3  7634  ltsopi  7687  recexnq  7757  recmulnqg  7758  ltsonq  7765  lt2addnq  7771  lt2mulnq  7772  ltbtwnnqq  7782  prarloclemarch2  7786  enq0sym  7799  enq0ref  7800  enq0tr  7801  enq0breq  7803  addnq0mo  7814  mulnq0mo  7815  addnnnq0  7816  mulnnnq0  7817  nqnq0a  7821  nqnq0m  7822  elinp  7841  prcdnql  7851  prcunqu  7852  prltlu  7854  prdisj  7859  prarloclemlo  7861  prarloclem3  7864  prarloclem5  7867  ltdfpr  7873  genprndl  7888  genprndu  7889  genpdisj  7890  appdivnq  7930  ltpopr  7962  ltexprlemdisj  7973  ltexprlemloc  7974  ltexprlemrl  7977  ltexprlemru  7979  ltexpri  7980  recexprlemm  7991  recexprlemdisj  7997  recexprlemloc  7998  recexprlem1ssl  8000  recexprlem1ssu  8001  recexpr  8005  aptiprleml  8006  archpr  8010  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  cauappcvgprlem1  8026  cauappcvgprlemlim  8028  cauappcvgpr  8029  caucvgprlemnkj  8033  caucvgprlemnbj  8034  caucvgprlemcl  8043  caucvgpr  8049  caucvgprprlemcbv  8054  caucvgprprlemval  8055  caucvgprprlemopu  8066  caucvgprpr  8079  suplocexpr  8092  addsrmo  8110  mulsrmo  8111  addsrpr  8112  mulsrpr  8113  lttrsr  8129  recexgt0sr  8140  caucvgsrlemcau  8160  caucvgsrlemgt1  8162  caucvgsrlemoffcau  8165  caucvgsrlemoffres  8167  caucvgsr  8169  suplocsrlem  8175  ltresr  8206  pitonn  8215  peano1nnnn  8219  peano2nnnn  8220  axprecex  8247  axcnre  8248  axpre-lttrn  8251  peano5nnnn  8259  axcaucvglemcau  8265  axcaucvglemres  8266  axpre-suploclemres  8268  axpre-suploc  8269  axlttrn  8394  axsuploc  8398  letri3  8406  letr  8408  le2add  8772  lt2add  8773  ltleadd  8774  lt2sub  8788  le2sub  8789  apreap  8915  apreim  8931  apti  8950  msq11  9232  dfinfre  9286  sup3exmid  9287  cju  9291  peano5nni  9307  1nn  9315  peano2nn  9316  nn2ge  9337  nominpos  9543  elz2  9716  dfuzi  9756  uzind  9757  supinfneg  9995  infsupneg  9996  elpqb  10050  xrletri3  10206  xrletr  10210  z2ge  10228  elixx1  10299  elioo2  10323  iooshf  10354  iooneg  10390  iccneg  10391  icoshft  10392  elfz1  10416  fzdifsuc  10488  fzrev  10491  1fv  10546  zsupcllemstep  10662  infssuzex  10666  nninfdcex  10672  zsupssdc  10673  exbtwnzlemstep  10682  exbtwnzlemshrink  10683  exbtwnzlemex  10684  exbtwnz  10685  rebtwn2zlemstep  10687  rebtwn2zlemshrink  10688  rebtwn2z  10689  qbtwnre  10691  qbtwnxr  10692  flval  10707  flqlelt  10711  flqbi  10725  flqbi2  10726  modqid2  10788  q2submod  10822  seqf1og  10958  nnesq  11097  hashunlem  11244  hashfibclem  11282  hashf1lem1  11285  hashf1lem2  11286  zfz1isolem1  11292  zfz1iso  11293  seq3coll  11294  fundm2domnop0  11300  pfxsuffeqwrdeq  11470  swrdpfx  11479  wrd2ind  11495  swrdccatin2  11501  swrdccatin2d  11516  pfxccatin12d  11517  reuccatpfxs1lem  11518  reuccatpfxs1  11519  shftlem  11581  shftfibg  11585  shftfib  11588  shftfn  11589  2shfti  11596  cjval  11610  cjth  11611  remim  11625  caucvgrelemcau  11746  caucvgre  11747  cvg1nlemcau  11750  cvg1nlemres  11751  rexanuz2  11757  recvguniq  11761  resqrexlemgt0  11786  resqrexlemoverl  11787  resqrexlemglsq  11788  resqrexlemsqa  11790  resqrexlemex  11791  rsqrmo  11793  resqrtcl  11795  rersqrtthlem  11796  absdiflt  11858  absdifle  11859  cau3lem  11880  icodiamlt  11946  maxleast  11979  negfi  11994  minmax  11996  lemininf  12000  ltmininf  12001  xrmaxlesup  12025  xrminmax  12031  xrltmininf  12036  xrlemininf  12037  iooinsup  12043  clim  12047  clim2  12049  climshftlemg  12068  addcn2  12076  climcau  12113  summodc  12150  fsum3  12154  fsum2dlemstep  12201  fisumcom2  12205  fsum00  12229  ntrivcvgap0  12316  prodeq1f  12319  prodeq2w  12323  prodeq2  12324  prodmodc  12345  zproddc  12346  fprodseq  12350  fprodntrivap  12351  fprod2dlemstep  12389  fprodcom2fi  12393  sin01bnd  12524  cos01bnd  12525  divalgmod  12694  ndvdssub  12697  gcdsupex  12734  gcdsupcl  12735  gcddvds  12740  dvdslegcd  12741  bezoutlemmain  12775  bezoutlemex  12778  bezoutlemzz  12779  bezoutlemeu  12784  bezoutlemle  12785  bezoutlemsup  12786  dfgcd3  12787  dfgcd2  12791  gcddiv  12796  lcmval  12841  lcmcllem  12845  dvdslcm  12847  lcmledvds  12848  lcmgcdlem  12855  lcmdvds  12857  coprmgcdb  12866  ncoprmgcdne1b  12867  coprmdvds1  12869  qredeu  12875  divgcdcoprm0  12879  divgcdcoprmex  12880  isprm3  12896  pw2dvdslemn  12943  pw2dvdseu  12946  oddpwdclemxy  12947  qnumdencl  12965  qnumdenbi  12970  crth  13002  reumodprminv  13032  pythagtriplem19  13061  pceu  13074  pczpre  13076  pcdiv  13081  pc11  13110  dvdsprmpweqle  13116  prmpwdvds  13134  pockthi  13137  infpnlem2  13139  elgz  13150  4sqlem12  13181  ennnfonelemim  13315  exmidunben  13317  ctinfom  13319  ctiunctlemu1st  13325  ctiunctlemu2nd  13326  ctiunctlemudc  13328  ctiunctlemfo  13330  infpn2  13347  ptex  13618  f1ocpbllem  13631  ercpbl  13652  erlecpbl  13653  grpidvalg  13693  grpidpropdg  13694  mgmlrid  13699  gzsumvalx  13709  gzsumfzval  13711  gzsumress  13712  gzsumval2  13714  issgrpd  13727  sgrppropd  13728  ismnddef  13731  sgrpidmndm  13733  ismndd  13750  mndpropd  13753  mndinvmod  13758  mnd1  13762  ismhm  13768  mhmex  13769  mhmpropd  13773  issubm  13779  insubm  13792  grppropd  13822  dfgrp2  13832  isgrpid2  13845  isgrpinv  13859  grplrinv  13862  grpidinv2  13863  grpidinv  13864  dfgrp3mlem  13903  grplactcnv  13907  releqgg  14023  eqgex  14024  eqgfval  14025  eqgval  14026  isghm  14046  ghmrn  14060  resghm  14063  ghmpropd  14086  cmnpropd  14098  ablpropd  14099  imasabl  14140  gsumvalfi  14152  prdsval  14173  isrng  14233  rngdi  14239  rngdir  14240  rngpropd  14254  rng1zrlem  14258  dfur2g  14266  issrg  14269  srgideu  14276  srgidmlem  14282  issrgid  14285  isring  14304  ringideu  14321  ringidmlem  14327  isringid  14330  ringid  14331  ringpropd  14343  ring1  14364  oppr0g  14387  oppr1g  14388  dvdsrvald  14400  dvdsrd  14401  dvdsrtr  14408  unitgrp  14423  dvdsrpropdg  14454  unitpropdg  14455  rhmopp  14483  opprnzrbg  14492  opprlring  14504  opprsubrngg  14519  issubrg  14529  subrg1  14539  subrgugrp  14548  resrhm2b  14557  subrgpropd  14561  rhmpropd  14562  opprdomnbg  14583  aprval  14591  aprap  14598  aprprop  14601  opprdrng  14620  islmod  14627  lmodlema  14628  islmodd  14629  lmodfopnelem2  14662  lmodprop2d  14685  islssm  14694  islssmg  14695  rnglidlrng  14835  isridl  14841  df2idl2rng  14845  quscrng  14870  isassa  15002  assalem  15003  isassad  15011  assapropd  15014  istopg  15100  fiinbas  15150  eltg2  15154  topbas  15168  neiint  15246  neipsm  15255  opnneissb  15256  opnssneib  15257  innei  15264  restbasg  15269  iscnp4  15319  cnpnei  15320  cnconst2  15334  cnptopresti  15339  cnptoprest  15340  cnpdis  15343  lmss  15347  lmres  15349  txbas  15359  eltx  15360  neitx  15369  txcnp  15372  txcnmpt  15374  uptx  15375  txdis  15378  txdis1cn  15379  txlm  15380  txhmeo  15420  ispsmet  15424  ismet  15445  isxmet  15446  bldisj  15502  blininf  15525  blssexps  15530  blssex  15531  ssblex  15532  xmspropd  15578  mspropd  15579  neibl  15592  metequiv  15596  bdmopn  15605  metrest  15607  xmetxp  15608  xmetxpbl  15609  xmettx  15611  metcnp3  15612  tgioo  15655  tgqioo  15656  addcncntoplem  15662  mpomulcn  15667  mulcncflem  15708  dedekindeu  15724  dedekindicclemicc  15733  limccl  15760  ellimc3apf  15761  limcimolemlt  15765  limccoap  15779  elply2  15836  sin0pilem2  15883  sincosq1sgn  15927  sincosq2sgn  15928  sincosq3sgn  15929  sincosq4sgn  15930  pellexlem3  16093  perfect  16115  lgsval  16123  lgsdir2lem5  16151  lgsne0  16157  lgsquadlem1  16196  lgsquadlem2  16197  lgsquadlem3  16198  lgsquad  16199  2lgslem3  16220  2sqlem8a  16241  2sqlem8  16242  2sqlem9  16243  gropd  16288  grstructd2dom  16289  incistruhgr  16331  uhgr2edg  16447  vtxd0nedgbfi  16540  wlkeq  16595  istrl  16626  clwwlkn2  16662  eupthsg  16686  iseupth  16688  eupth2lem1  16699  depind  16750  bj-sseq  16820  bj-charfunbi  16837  bj-nalset  16921  bj-indeq  16955  bj-2inf  16964  strcoll2  17009  strcollnft  17010  strcollnfALT  17012  sscoll2  17014  subctctexmid  17030  domomsubct  17031  exmidsbthrlem  17067  sbthom  17071  qdencn  17072  qdiff  17098  ltlenmkv  17120  alsbid  17143