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  905  orbididc  955  3anbi123d  1323  xorbi2d  1391  xorbi1d  1392  drsb1  1813  mopick  2123  clelab  2322  cbvrexfw  2720  cbvrexf  2722  cbvreu  2727  cbvrexvw  2734  cbvreuvw  2735  cbvrexdva2  2737  cbvrab  2761  gencbvex  2810  rspce  2863  eqvincf  2889  ceqsrexv  2894  elrabf  2918  rexab2  2930  reu2  2952  reu6  2953  rmo4  2957  reu8  2960  reuind  2969  sbcan  3032  sbcang  3033  sbcabel  3071  rmob  3082  cbvrexcsf  3148  cbvreucsf  3149  cbvrabcsf  3150  difjust  3158  injust  3162  eldif  3166  ssconb  3296  elin  3346  opeq1  3808  opeq2  3809  2ralunsn  3828  elunii  3844  csbunig  3847  eluniab  3851  cbvopab  4104  cbvopab1  4106  cbvopab2  4107  cbvopab1s  4108  cbvopab2v  4110  cbvmptf  4127  cbvmpt  4128  trel  4138  nalset  4163  elssabg  4181  mss  4259  exss  4260  opelopab2a  4299  poeq1  4334  pocl  4338  soeq1  4350  weeq1  4391  weeq2  4392  ordeq  4407  zfun  4469  snnex  4483  reusv3  4495  ontr2exmid  4561  regexmid  4571  onintexmid  4609  reg3exmid  4616  peano5  4634  limom  4650  nnregexmid  4657  vtoclr  4711  opeliunxp  4718  poinxp  4732  opbrop  4742  csbxpg  4744  opeliunxp2  4806  relop  4816  brcogw  4835  elrnmpt1  4917  elsnres  4983  dfres2  4998  inimasn  5087  xpcanm  5109  xpcan2m  5110  elxp4  5157  elxp5  5158  cnvsom  5213  sbcfung  5282  funopg  5292  fununi  5326  funcnvuni  5327  fneq1  5346  2elresin  5369  feq1  5390  sbcfng  5405  sbcfg  5406  f1eq1  5458  foeq1  5476  f1oeq1  5492  f1oeq2  5493  f1oeq3  5494  ffoss  5536  brprcneu  5551  fv3  5581  tz6.12f  5587  ssimaex  5622  fvopab3g  5634  fvopab3ig  5635  fvopab6  5658  fmptco  5728  elunirn  5813  f1imaeq  5822  foeqcnvco  5837  fliftfun  5843  fliftval  5847  isoeq1  5848  isoeq4  5851  isoini  5865  isopolem  5869  f1oiso2  5874  riotabidv  5879  cbvriota  5888  acexmid  5921  ovanraleqv  5946  cbvoprab1  5994  cbvoprab2  5995  cbvoprab12  5996  cbvmpox  6000  ov  6042  ovig  6044  ovg  6062  caovimo  6117  caoftrn  6163  opabex3d  6178  opabex3  6179  uchoice  6195  elxp6  6227  unielxp  6232  dfoprab4  6250  dfoprab4f  6251  fmpox  6258  xporderlem  6289  poxp  6290  cnvoprab  6292  f1od2  6293  opeliunxp2f  6296  rbropapd  6300  dftpos4  6321  tpostpos  6322  smoiso  6360  tfrlem3ag  6367  tfrlem3a  6368  tfr0dm  6380  tfrlemisucaccv  6383  tfrlemiex  6389  tfrlemi1  6390  tfrlemi14d  6391  tfrexlem  6392  tfr1onlem3ag  6395  tfr1onlemsucaccv  6399  tfr1onlemex  6405  tfr1onlemaccex  6406  tfr1onlemres  6407  tfrcllemsucaccv  6412  tfrcllembxssdm  6414  tfrcllemex  6418  tfrcllemaccex  6419  tfrcllemres  6420  tfrcldm  6421  frec0g  6455  frecabcl  6457  freccllem  6460  frecfcllem  6462  frecsuclem  6464  frecsuc  6465  nnacan  6570  nnmcan  6577  nnaordex  6586  ertr  6607  brecop  6684  eroveu  6685  ecopovtrn  6691  ecopovtrng  6694  th3qlem1  6696  th3qlem2  6697  th3q  6699  elpm2r  6725  mapsncnv  6754  elixp2  6761  ixpeq1  6768  elixpsn  6794  ixpsnf1o  6795  mapsnen  6870  map1  6871  xpsnen  6880  endisj  6883  pw2f1odclem  6895  xpf1o  6905  phplem3g  6917  ssfiexmid  6937  domfiexmid  6939  findcard2s  6951  isinfinf  6958  ac6sfi  6959  fiintim  6992  fisseneq  6995  opabfi  6999  f1dmvrnfibi  7010  sbthlem2  7024  isbth  7033  supeq1  7052  supeq3  7056  supeq123d  7057  supmoti  7059  eqsupti  7062  supsnti  7071  isotilem  7072  isoti  7073  supisolem  7074  supisoex  7075  cnvinfex  7084  cnvti  7085  eqinfti  7086  infvalti  7088  updjud  7148  ctssexmid  7216  omniwomnimkv  7233  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  acfun  7274  tapeq1  7319  tapeq2  7320  exmidapne  7327  ccfunen  7331  cc2lem  7333  cc3  7335  ltsopi  7387  recexnq  7457  recmulnqg  7458  ltsonq  7465  lt2addnq  7471  lt2mulnq  7472  ltbtwnnqq  7482  prarloclemarch2  7486  enq0sym  7499  enq0ref  7500  enq0tr  7501  enq0breq  7503  addnq0mo  7514  mulnq0mo  7515  addnnnq0  7516  mulnnnq0  7517  nqnq0a  7521  nqnq0m  7522  elinp  7541  prcdnql  7551  prcunqu  7552  prltlu  7554  prdisj  7559  prarloclemlo  7561  prarloclem3  7564  prarloclem5  7567  ltdfpr  7573  genprndl  7588  genprndu  7589  genpdisj  7590  appdivnq  7630  ltpopr  7662  ltexprlemdisj  7673  ltexprlemloc  7674  ltexprlemrl  7677  ltexprlemru  7679  ltexpri  7680  recexprlemm  7691  recexprlemdisj  7697  recexprlemloc  7698  recexprlem1ssl  7700  recexprlem1ssu  7701  recexpr  7705  aptiprleml  7706  archpr  7710  cauappcvgprlemladdru  7723  cauappcvgprlemladdrl  7724  cauappcvgprlem1  7726  cauappcvgprlemlim  7728  cauappcvgpr  7729  caucvgprlemnkj  7733  caucvgprlemnbj  7734  caucvgprlemcl  7743  caucvgpr  7749  caucvgprprlemcbv  7754  caucvgprprlemval  7755  caucvgprprlemopu  7766  caucvgprpr  7779  suplocexpr  7792  addsrmo  7810  mulsrmo  7811  addsrpr  7812  mulsrpr  7813  lttrsr  7829  recexgt0sr  7840  caucvgsrlemcau  7860  caucvgsrlemgt1  7862  caucvgsrlemoffcau  7865  caucvgsrlemoffres  7867  caucvgsr  7869  suplocsrlem  7875  ltresr  7906  pitonn  7915  peano1nnnn  7919  peano2nnnn  7920  axprecex  7947  axcnre  7948  axpre-lttrn  7951  peano5nnnn  7959  axcaucvglemcau  7965  axcaucvglemres  7966  axpre-suploclemres  7968  axpre-suploc  7969  axlttrn  8095  axsuploc  8099  letri3  8107  letr  8109  le2add  8471  lt2add  8472  ltleadd  8473  lt2sub  8487  le2sub  8488  apreap  8614  apreim  8630  apti  8649  msq11  8929  dfinfre  8983  sup3exmid  8984  cju  8988  peano5nni  8993  1nn  9001  peano2nn  9002  nn2ge  9023  nominpos  9229  elz2  9397  dfuzi  9436  uzind  9437  supinfneg  9669  infsupneg  9670  elpqb  9724  xrletri3  9879  xrletr  9883  z2ge  9901  elixx1  9972  elioo2  9996  iooshf  10027  iooneg  10063  iccneg  10064  icoshft  10065  elfz1  10088  fzdifsuc  10156  fzrev  10159  1fv  10214  zsupcllemstep  10319  infssuzex  10323  nninfdcex  10327  zsupssdc  10328  exbtwnzlemstep  10337  exbtwnzlemshrink  10338  exbtwnzlemex  10339  exbtwnz  10340  rebtwn2zlemstep  10342  rebtwn2zlemshrink  10343  rebtwn2z  10344  qbtwnre  10346  qbtwnxr  10347  flval  10362  flqlelt  10366  flqbi  10380  flqbi2  10381  modqid2  10443  q2submod  10477  seqf1og  10613  nnesq  10751  hashunlem  10896  zfz1isolem1  10932  zfz1iso  10933  seq3coll  10934  shftlem  10981  shftfibg  10985  shftfib  10988  shftfn  10989  2shfti  10996  cjval  11010  cjth  11011  remim  11025  caucvgrelemcau  11145  caucvgre  11146  cvg1nlemcau  11149  cvg1nlemres  11150  rexanuz2  11156  recvguniq  11160  resqrexlemgt0  11185  resqrexlemoverl  11186  resqrexlemglsq  11187  resqrexlemsqa  11189  resqrexlemex  11190  rsqrmo  11192  resqrtcl  11194  rersqrtthlem  11195  absdiflt  11257  absdifle  11258  cau3lem  11279  icodiamlt  11345  maxleast  11378  negfi  11393  minmax  11395  lemininf  11399  ltmininf  11400  xrmaxlesup  11424  xrminmax  11430  xrltmininf  11435  xrlemininf  11436  iooinsup  11442  clim  11446  clim2  11448  climshftlemg  11467  addcn2  11475  climcau  11512  summodc  11548  fsum3  11552  fsum2dlemstep  11599  fisumcom2  11603  fsum00  11627  ntrivcvgap0  11714  prodeq1f  11717  prodeq2w  11721  prodeq2  11722  prodmodc  11743  zproddc  11744  fprodseq  11748  fprodntrivap  11749  fprod2dlemstep  11787  fprodcom2fi  11791  sin01bnd  11922  cos01bnd  11923  divalgmod  12092  ndvdssub  12095  gcdsupex  12124  gcdsupcl  12125  gcddvds  12130  dvdslegcd  12131  bezoutlemmain  12165  bezoutlemex  12168  bezoutlemzz  12169  bezoutlemeu  12174  bezoutlemle  12175  bezoutlemsup  12176  dfgcd3  12177  dfgcd2  12181  gcddiv  12186  lcmval  12231  lcmcllem  12235  dvdslcm  12237  lcmledvds  12238  lcmgcdlem  12245  lcmdvds  12247  coprmgcdb  12256  ncoprmgcdne1b  12257  coprmdvds1  12259  qredeu  12265  divgcdcoprm0  12269  divgcdcoprmex  12270  isprm3  12286  pw2dvdslemn  12333  pw2dvdseu  12336  oddpwdclemxy  12337  qnumdencl  12355  qnumdenbi  12360  crth  12392  reumodprminv  12422  pythagtriplem19  12451  pceu  12464  pczpre  12466  pcdiv  12471  pc11  12500  dvdsprmpweqle  12506  prmpwdvds  12524  pockthi  12527  infpnlem2  12529  elgz  12540  4sqlem12  12571  ennnfonelemim  12641  exmidunben  12643  ctinfom  12645  ctiunctlemu1st  12651  ctiunctlemu2nd  12652  ctiunctlemudc  12654  ctiunctlemfo  12656  infpn2  12673  ptex  12935  f1ocpbllem  12953  ercpbl  12974  erlecpbl  12975  grpidvalg  13016  grpidpropdg  13017  mgmlrid  13022  igsumvalx  13032  gsumfzval  13034  gsumress  13038  gsumval2  13040  issgrpd  13055  sgrppropd  13056  ismnddef  13059  sgrpidmndm  13061  ismndd  13078  mndpropd  13081  mndinvmod  13086  mnd1  13087  ismhm  13093  mhmex  13094  mhmpropd  13098  issubm  13104  insubm  13117  grppropd  13149  dfgrp2  13159  isgrpid2  13172  isgrpinv  13186  grplrinv  13189  grpidinv2  13190  grpidinv  13191  dfgrp3mlem  13230  grplactcnv  13234  releqgg  13350  eqgex  13351  eqgfval  13352  eqgval  13353  isghm  13373  ghmrn  13387  resghm  13390  ghmpropd  13413  cmnpropd  13425  ablpropd  13426  imasabl  13466  isrng  13490  rngdi  13496  rngdir  13497  rngpropd  13511  dfur2g  13518  issrg  13521  srgideu  13528  srgidmlem  13534  issrgid  13537  srg1zr  13543  isring  13556  ringideu  13573  ringidmlem  13578  isringid  13581  ringid  13582  ringpropd  13594  ring1  13615  oppr0g  13637  oppr1g  13638  reldvdsrsrg  13648  dvdsrvald  13649  dvdsrd  13650  dvdsrtr  13657  unitgrp  13672  dvdsrpropdg  13703  unitpropdg  13704  rhmopp  13732  opprnzrbg  13741  opprsubrngg  13767  issubrg  13777  subrg1  13787  subrgugrp  13796  resrhm2b  13805  subrgpropd  13809  rhmpropd  13810  opprdomnbg  13830  aprval  13838  aprap  13842  islmod  13847  lmodlema  13848  islmodd  13849  lmodfopnelem2  13881  lmodprop2d  13904  islssm  13913  islssmg  13914  rnglidlrng  14054  isridl  14060  df2idl2rng  14064  quscrng  14089  istopg  14235  fiinbas  14285  eltg2  14289  topbas  14303  neiint  14381  neipsm  14390  opnneissb  14391  opnssneib  14392  innei  14399  restbasg  14404  iscnp4  14454  cnpnei  14455  cnconst2  14469  cnptopresti  14474  cnptoprest  14475  cnpdis  14478  lmss  14482  lmres  14484  txbas  14494  eltx  14495  neitx  14504  txcnp  14507  txcnmpt  14509  uptx  14510  txdis  14513  txdis1cn  14514  txlm  14515  txhmeo  14555  ispsmet  14559  ismet  14580  isxmet  14581  bldisj  14637  blininf  14660  blssexps  14665  blssex  14666  ssblex  14667  xmspropd  14713  mspropd  14714  neibl  14727  metequiv  14731  bdmopn  14740  metrest  14742  xmetxp  14743  xmetxpbl  14744  xmettx  14746  metcnp3  14747  tgioo  14790  tgqioo  14791  addcncntoplem  14797  mpomulcn  14802  mulcncflem  14843  dedekindeu  14859  dedekindicclemicc  14868  limccl  14895  ellimc3apf  14896  limcimolemlt  14900  limccoap  14914  elply2  14971  sin0pilem2  15018  sincosq1sgn  15062  sincosq2sgn  15063  sincosq3sgn  15064  sincosq4sgn  15065  perfect  15237  lgsval  15245  lgsdir2lem5  15273  lgsne0  15279  lgsquadlem1  15318  lgsquadlem2  15319  lgsquadlem3  15320  lgsquad  15321  2lgslem3  15342  2sqlem8a  15363  2sqlem8  15364  2sqlem9  15365  bj-sseq  15438  bj-charfunbi  15457  bj-nalset  15541  bj-indeq  15575  bj-2inf  15584  strcoll2  15629  strcollnft  15630  strcollnfALT  15632  sscoll2  15634  subctctexmid  15645  exmidsbthrlem  15666  sbthom  15670  qdencn  15671  ltlenmkv  15714