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  605  pm5.17dc  906  orbididc  956  3anbi123d  1325  xorbi2d  1400  xorbi1d  1401  drsb1  1822  mopick  2132  clelab  2331  cbvrexfw  2729  cbvrexf  2731  cbvreu  2736  cbvrexvw  2743  cbvreuvw  2744  cbvrexdva2  2746  cbvrab  2770  gencbvex  2819  rspce  2872  eqvincf  2898  ceqsrexv  2903  elrabf  2927  rexab2  2939  reu2  2961  reu6  2962  rmo4  2966  reu8  2969  reuind  2978  sbcan  3041  sbcang  3042  sbcabel  3080  rmob  3091  cbvrexcsf  3157  cbvreucsf  3158  cbvrabcsf  3159  difjust  3167  injust  3171  eldif  3175  ssconb  3306  elin  3356  opeq1  3819  opeq2  3820  2ralunsn  3839  elunii  3855  csbunig  3858  eluniab  3862  cbvopab  4116  cbvopab1  4118  cbvopab2  4119  cbvopab1s  4120  cbvopab2v  4122  cbvmptf  4139  cbvmpt  4140  trel  4150  nalset  4175  elssabg  4193  mss  4271  exss  4272  opelopab2a  4312  poeq1  4347  pocl  4351  soeq1  4363  weeq1  4404  weeq2  4405  ordeq  4420  zfun  4482  snnex  4496  reusv3  4508  ontr2exmid  4574  regexmid  4584  onintexmid  4622  reg3exmid  4629  peano5  4647  limom  4663  nnregexmid  4670  vtoclr  4724  opeliunxp  4731  poinxp  4745  opbrop  4755  csbxpg  4757  opeliunxp2  4819  relop  4829  brcogw  4848  elrnmpt1  4930  elsnres  4997  dfres2  5012  inimasn  5101  xpcanm  5123  xpcan2m  5124  elxp4  5171  elxp5  5172  cnvsom  5227  sbcfung  5296  funopg  5306  fununi  5343  funcnvuni  5344  fneq1  5363  2elresin  5388  feq1  5410  sbcfng  5425  sbcfg  5426  f1eq1  5478  foeq1  5496  f1oeq1  5512  f1oeq2  5513  f1oeq3  5514  ffoss  5556  brprcneu  5571  fv3  5601  tz6.12f  5607  ssimaex  5642  fvopab3g  5654  fvopab3ig  5655  fvopab6  5678  fmptco  5748  funopsn  5764  funopdmsn  5766  elunirn  5837  f1imaeq  5846  foeqcnvco  5861  fliftfun  5867  fliftval  5871  isoeq1  5872  isoeq4  5875  isoini  5889  isopolem  5893  f1oiso2  5898  riotabidv  5903  cbvriota  5912  acexmid  5945  ovanraleqv  5970  cbvoprab1  6019  cbvoprab2  6020  cbvoprab12  6021  cbvmpox  6025  ov  6067  ovig  6069  ovg  6087  caovimo  6142  caoftrn  6193  opabex3d  6208  opabex3  6209  uchoice  6225  elxp6  6257  unielxp  6262  dfoprab4  6280  dfoprab4f  6281  fmpox  6288  xporderlem  6319  poxp  6320  cnvoprab  6322  f1od2  6323  opeliunxp2f  6326  rbropapd  6330  dftpos4  6351  tpostpos  6352  smoiso  6390  tfrlem3ag  6397  tfrlem3a  6398  tfr0dm  6410  tfrlemisucaccv  6413  tfrlemiex  6419  tfrlemi1  6420  tfrlemi14d  6421  tfrexlem  6422  tfr1onlem3ag  6425  tfr1onlemsucaccv  6429  tfr1onlemex  6435  tfr1onlemaccex  6436  tfr1onlemres  6437  tfrcllemsucaccv  6442  tfrcllembxssdm  6444  tfrcllemex  6448  tfrcllemaccex  6449  tfrcllemres  6450  tfrcldm  6451  frec0g  6485  frecabcl  6487  freccllem  6490  frecfcllem  6492  frecsuclem  6494  frecsuc  6495  nnacan  6600  nnmcan  6607  nnaordex  6616  ertr  6637  brecop  6714  eroveu  6715  ecopovtrn  6721  ecopovtrng  6724  th3qlem1  6726  th3qlem2  6727  th3q  6729  elpm2r  6755  mapsncnv  6784  elixp2  6791  ixpeq1  6798  elixpsn  6824  ixpsnf1o  6825  mapsnen  6905  map1  6906  xpsnen  6918  endisj  6921  pw2f1odclem  6933  xpf1o  6943  phplem3g  6955  ssfiexmid  6975  domfiexmid  6977  findcard2s  6989  isinfinf  6996  ac6sfi  6997  fiintim  7030  fisseneq  7033  opabfi  7037  f1dmvrnfibi  7048  sbthlem2  7062  isbth  7071  supeq1  7090  supeq3  7094  supeq123d  7095  supmoti  7097  eqsupti  7100  supsnti  7109  isotilem  7110  isoti  7111  supisolem  7112  supisoex  7113  cnvinfex  7122  cnvti  7123  eqinfti  7124  infvalti  7126  updjud  7186  ctssexmid  7254  omniwomnimkv  7271  exmidfodomrlemr  7312  exmidfodomrlemrALT  7313  acneq  7316  acfun  7321  tapeq1  7366  tapeq2  7367  exmidapne  7374  ccfunen  7378  cc2lem  7380  cc3  7382  ltsopi  7435  recexnq  7505  recmulnqg  7506  ltsonq  7513  lt2addnq  7519  lt2mulnq  7520  ltbtwnnqq  7530  prarloclemarch2  7534  enq0sym  7547  enq0ref  7548  enq0tr  7549  enq0breq  7551  addnq0mo  7562  mulnq0mo  7563  addnnnq0  7564  mulnnnq0  7565  nqnq0a  7569  nqnq0m  7570  elinp  7589  prcdnql  7599  prcunqu  7600  prltlu  7602  prdisj  7607  prarloclemlo  7609  prarloclem3  7612  prarloclem5  7615  ltdfpr  7621  genprndl  7636  genprndu  7637  genpdisj  7638  appdivnq  7678  ltpopr  7710  ltexprlemdisj  7721  ltexprlemloc  7722  ltexprlemrl  7725  ltexprlemru  7727  ltexpri  7728  recexprlemm  7739  recexprlemdisj  7745  recexprlemloc  7746  recexprlem1ssl  7748  recexprlem1ssu  7749  recexpr  7753  aptiprleml  7754  archpr  7758  cauappcvgprlemladdru  7771  cauappcvgprlemladdrl  7772  cauappcvgprlem1  7774  cauappcvgprlemlim  7776  cauappcvgpr  7777  caucvgprlemnkj  7781  caucvgprlemnbj  7782  caucvgprlemcl  7791  caucvgpr  7797  caucvgprprlemcbv  7802  caucvgprprlemval  7803  caucvgprprlemopu  7814  caucvgprpr  7827  suplocexpr  7840  addsrmo  7858  mulsrmo  7859  addsrpr  7860  mulsrpr  7861  lttrsr  7877  recexgt0sr  7888  caucvgsrlemcau  7908  caucvgsrlemgt1  7910  caucvgsrlemoffcau  7913  caucvgsrlemoffres  7915  caucvgsr  7917  suplocsrlem  7923  ltresr  7954  pitonn  7963  peano1nnnn  7967  peano2nnnn  7968  axprecex  7995  axcnre  7996  axpre-lttrn  7999  peano5nnnn  8007  axcaucvglemcau  8013  axcaucvglemres  8014  axpre-suploclemres  8016  axpre-suploc  8017  axlttrn  8143  axsuploc  8147  letri3  8155  letr  8157  le2add  8519  lt2add  8520  ltleadd  8521  lt2sub  8535  le2sub  8536  apreap  8662  apreim  8678  apti  8697  msq11  8977  dfinfre  9031  sup3exmid  9032  cju  9036  peano5nni  9041  1nn  9049  peano2nn  9050  nn2ge  9071  nominpos  9277  elz2  9446  dfuzi  9485  uzind  9486  supinfneg  9718  infsupneg  9719  elpqb  9773  xrletri3  9928  xrletr  9932  z2ge  9950  elixx1  10021  elioo2  10045  iooshf  10076  iooneg  10112  iccneg  10113  icoshft  10114  elfz1  10137  fzdifsuc  10205  fzrev  10208  1fv  10263  zsupcllemstep  10374  infssuzex  10378  nninfdcex  10382  zsupssdc  10383  exbtwnzlemstep  10392  exbtwnzlemshrink  10393  exbtwnzlemex  10394  exbtwnz  10395  rebtwn2zlemstep  10397  rebtwn2zlemshrink  10398  rebtwn2z  10399  qbtwnre  10401  qbtwnxr  10402  flval  10417  flqlelt  10421  flqbi  10435  flqbi2  10436  modqid2  10498  q2submod  10532  seqf1og  10668  nnesq  10806  hashunlem  10951  zfz1isolem1  10987  zfz1iso  10988  seq3coll  10989  fundm2domnop0  10992  pfxsuffeqwrdeq  11152  shftlem  11160  shftfibg  11164  shftfib  11167  shftfn  11168  2shfti  11175  cjval  11189  cjth  11190  remim  11204  caucvgrelemcau  11324  caucvgre  11325  cvg1nlemcau  11328  cvg1nlemres  11329  rexanuz2  11335  recvguniq  11339  resqrexlemgt0  11364  resqrexlemoverl  11365  resqrexlemglsq  11366  resqrexlemsqa  11368  resqrexlemex  11369  rsqrmo  11371  resqrtcl  11373  rersqrtthlem  11374  absdiflt  11436  absdifle  11437  cau3lem  11458  icodiamlt  11524  maxleast  11557  negfi  11572  minmax  11574  lemininf  11578  ltmininf  11579  xrmaxlesup  11603  xrminmax  11609  xrltmininf  11614  xrlemininf  11615  iooinsup  11621  clim  11625  clim2  11627  climshftlemg  11646  addcn2  11654  climcau  11691  summodc  11727  fsum3  11731  fsum2dlemstep  11778  fisumcom2  11782  fsum00  11806  ntrivcvgap0  11893  prodeq1f  11896  prodeq2w  11900  prodeq2  11901  prodmodc  11922  zproddc  11923  fprodseq  11927  fprodntrivap  11928  fprod2dlemstep  11966  fprodcom2fi  11970  sin01bnd  12101  cos01bnd  12102  divalgmod  12271  ndvdssub  12274  gcdsupex  12311  gcdsupcl  12312  gcddvds  12317  dvdslegcd  12318  bezoutlemmain  12352  bezoutlemex  12355  bezoutlemzz  12356  bezoutlemeu  12361  bezoutlemle  12362  bezoutlemsup  12363  dfgcd3  12364  dfgcd2  12368  gcddiv  12373  lcmval  12418  lcmcllem  12422  dvdslcm  12424  lcmledvds  12425  lcmgcdlem  12432  lcmdvds  12434  coprmgcdb  12443  ncoprmgcdne1b  12444  coprmdvds1  12446  qredeu  12452  divgcdcoprm0  12456  divgcdcoprmex  12457  isprm3  12473  pw2dvdslemn  12520  pw2dvdseu  12523  oddpwdclemxy  12524  qnumdencl  12542  qnumdenbi  12547  crth  12579  reumodprminv  12609  pythagtriplem19  12638  pceu  12651  pczpre  12653  pcdiv  12658  pc11  12687  dvdsprmpweqle  12693  prmpwdvds  12711  pockthi  12714  infpnlem2  12716  elgz  12727  4sqlem12  12758  ennnfonelemim  12828  exmidunben  12830  ctinfom  12832  ctiunctlemu1st  12838  ctiunctlemu2nd  12839  ctiunctlemudc  12841  ctiunctlemfo  12843  infpn2  12860  ptex  13129  prdsval  13138  f1ocpbllem  13175  ercpbl  13196  erlecpbl  13197  grpidvalg  13238  grpidpropdg  13239  mgmlrid  13244  igsumvalx  13254  gsumfzval  13256  gsumress  13260  gsumval2  13262  issgrpd  13277  sgrppropd  13278  ismnddef  13283  sgrpidmndm  13285  ismndd  13302  mndpropd  13305  mndinvmod  13310  mnd1  13320  ismhm  13326  mhmex  13327  mhmpropd  13331  issubm  13337  insubm  13350  grppropd  13382  dfgrp2  13392  isgrpid2  13405  isgrpinv  13419  grplrinv  13422  grpidinv2  13423  grpidinv  13424  dfgrp3mlem  13463  grplactcnv  13467  releqgg  13589  eqgex  13590  eqgfval  13591  eqgval  13592  isghm  13612  ghmrn  13626  resghm  13629  ghmpropd  13652  cmnpropd  13664  ablpropd  13665  imasabl  13705  isrng  13729  rngdi  13735  rngdir  13736  rngpropd  13750  dfur2g  13757  issrg  13760  srgideu  13767  srgidmlem  13773  issrgid  13776  srg1zr  13782  isring  13795  ringideu  13812  ringidmlem  13817  isringid  13820  ringid  13821  ringpropd  13833  ring1  13854  oppr0g  13876  oppr1g  13877  reldvdsrsrg  13887  dvdsrvald  13888  dvdsrd  13889  dvdsrtr  13896  unitgrp  13911  dvdsrpropdg  13942  unitpropdg  13943  rhmopp  13971  opprnzrbg  13980  opprsubrngg  14006  issubrg  14016  subrg1  14026  subrgugrp  14035  resrhm2b  14044  subrgpropd  14048  rhmpropd  14049  opprdomnbg  14069  aprval  14077  aprap  14081  islmod  14086  lmodlema  14087  islmodd  14088  lmodfopnelem2  14120  lmodprop2d  14143  islssm  14152  islssmg  14153  rnglidlrng  14293  isridl  14299  df2idl2rng  14303  quscrng  14328  istopg  14504  fiinbas  14554  eltg2  14558  topbas  14572  neiint  14650  neipsm  14659  opnneissb  14660  opnssneib  14661  innei  14668  restbasg  14673  iscnp4  14723  cnpnei  14724  cnconst2  14738  cnptopresti  14743  cnptoprest  14744  cnpdis  14747  lmss  14751  lmres  14753  txbas  14763  eltx  14764  neitx  14773  txcnp  14776  txcnmpt  14778  uptx  14779  txdis  14782  txdis1cn  14783  txlm  14784  txhmeo  14824  ispsmet  14828  ismet  14849  isxmet  14850  bldisj  14906  blininf  14929  blssexps  14934  blssex  14935  ssblex  14936  xmspropd  14982  mspropd  14983  neibl  14996  metequiv  15000  bdmopn  15009  metrest  15011  xmetxp  15012  xmetxpbl  15013  xmettx  15015  metcnp3  15016  tgioo  15059  tgqioo  15060  addcncntoplem  15066  mpomulcn  15071  mulcncflem  15112  dedekindeu  15128  dedekindicclemicc  15137  limccl  15164  ellimc3apf  15165  limcimolemlt  15169  limccoap  15183  elply2  15240  sin0pilem2  15287  sincosq1sgn  15331  sincosq2sgn  15332  sincosq3sgn  15333  sincosq4sgn  15334  perfect  15506  lgsval  15514  lgsdir2lem5  15542  lgsne0  15548  lgsquadlem1  15587  lgsquadlem2  15588  lgsquadlem3  15589  lgsquad  15590  2lgslem3  15611  2sqlem8a  15632  2sqlem8  15633  2sqlem9  15634  gropd  15677  grstructd2dom  15678  bj-sseq  15765  bj-charfunbi  15784  bj-nalset  15868  bj-indeq  15902  bj-2inf  15911  strcoll2  15956  strcollnft  15957  strcollnfALT  15959  sscoll2  15961  subctctexmid  15974  domomsubct  15975  exmidsbthrlem  15998  sbthom  16002  qdencn  16003  ltlenmkv  16046