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  607  pm5.17dc  909  orbididc  959  ifpbi123d  998  3anbi123d  1346  xorbi2d  1422  xorbi1d  1423  drsb1  1845  mopick  2156  clelab  2355  cbvrmow  2714  cbvrexfw  2755  cbvrexf  2757  cbvreu  2763  cbvrexvw  2770  cbvreuvw  2771  cbvrexdva2  2773  cbvrab  2797  gencbvex  2847  rspce  2902  eqvincf  2928  ceqsrexv  2933  elrabf  2957  rexab2  2969  reu2  2991  reu6  2992  rmo4  2996  reu8  2999  reuind  3008  sbcan  3071  sbcang  3072  reu8nf  3110  sbcabel  3111  rmob  3122  cbvrexcsf  3188  cbvreucsf  3189  cbvrabcsf  3190  difjust  3198  injust  3202  eldif  3206  ssconb  3337  elin  3387  opeq1  3857  opeq2  3858  2ralunsn  3877  elunii  3893  csbunig  3896  eluniab  3900  cbvopab  4155  cbvopab1  4157  cbvopab2  4158  cbvopab1s  4159  cbvopab2v  4161  cbvmptf  4178  cbvmpt  4179  trel  4189  nalset  4214  elssabg  4232  mss  4312  exss  4313  opelopab2a  4353  poeq1  4390  pocl  4394  soeq1  4406  weeq1  4447  weeq2  4448  ordeq  4463  zfun  4525  snnex  4539  reusv3  4551  ontr2exmid  4617  regexmid  4627  onintexmid  4665  reg3exmid  4672  peano5  4690  limom  4706  nnregexmid  4713  vtoclr  4767  opeliunxp  4774  poinxp  4788  opbrop  4798  csbxpg  4800  opeliunxp2  4862  relop  4872  brcogw  4891  elrnmpt1  4975  elsnres  5042  dfres2  5057  inimasn  5146  xpcanm  5168  xpcan2m  5169  elxp4  5216  elxp5  5217  cnvsom  5272  sbcfung  5342  funopg  5352  fununi  5389  funcnvuni  5390  fneq1  5409  2elresin  5434  feq1  5456  sbcfng  5471  sbcfg  5472  f1eq1  5526  foeq1  5544  f1oeq1  5560  f1oeq2  5561  f1oeq3  5562  ffoss  5604  brprcneu  5620  fv3  5650  tz6.12f  5656  ssimaex  5695  fvopab3g  5707  fvopab3ig  5708  fvopab6  5731  fmptco  5801  funopsn  5817  funopdmsn  5819  elunirn  5890  f1imaeq  5899  foeqcnvco  5914  fliftfun  5920  fliftval  5924  isoeq1  5925  isoeq4  5928  isoini  5942  isopolem  5946  f1oiso2  5951  riotabidv  5956  cbvriotavw  5965  cbvriota  5966  acexmid  6000  ovanraleqv  6025  cbvoprab1  6076  cbvoprab2  6077  cbvoprab12  6078  cbvmpox  6082  ov  6124  ovig  6126  ovg  6144  caovimo  6199  caoftrn  6251  opabex3d  6266  opabex3  6267  uchoice  6283  elxp6  6315  unielxp  6320  dfoprab4  6338  dfoprab4f  6339  fmpox  6346  xporderlem  6377  poxp  6378  cnvoprab  6380  f1od2  6381  opeliunxp2f  6384  rbropapd  6388  dftpos4  6409  tpostpos  6410  smoiso  6448  tfrlem3ag  6455  tfrlem3a  6456  tfr0dm  6468  tfrlemisucaccv  6471  tfrlemiex  6477  tfrlemi1  6478  tfrlemi14d  6479  tfrexlem  6480  tfr1onlem3ag  6483  tfr1onlemsucaccv  6487  tfr1onlemex  6493  tfr1onlemaccex  6494  tfr1onlemres  6495  tfrcllemsucaccv  6500  tfrcllembxssdm  6502  tfrcllemex  6506  tfrcllemaccex  6507  tfrcllemres  6508  tfrcldm  6509  frec0g  6543  frecabcl  6545  freccllem  6548  frecfcllem  6550  frecsuclem  6552  frecsuc  6553  nnacan  6658  nnmcan  6665  nnaordex  6674  ertr  6695  brecop  6772  eroveu  6773  ecopovtrn  6779  ecopovtrng  6782  th3qlem1  6784  th3qlem2  6785  th3q  6787  elpm2r  6813  mapsncnv  6842  elixp2  6849  ixpeq1  6856  elixpsn  6882  ixpsnf1o  6883  mapsnen  6964  map1  6965  xpsnen  6980  endisj  6983  pw2f1odclem  6995  xpf1o  7005  phplem3g  7017  ssfiexmid  7038  domfiexmid  7040  findcard2s  7052  isinfinf  7059  ac6sfi  7060  fiintim  7093  fisseneq  7096  opabfi  7100  f1dmvrnfibi  7111  sbthlem2  7125  isbth  7134  supeq1  7153  supeq3  7157  supeq123d  7158  supmoti  7160  eqsupti  7163  supsnti  7172  isotilem  7173  isoti  7174  supisolem  7175  supisoex  7176  cnvinfex  7185  cnvti  7186  eqinfti  7187  infvalti  7189  updjud  7249  ctssexmid  7317  omniwomnimkv  7334  exmidfodomrlemr  7380  exmidfodomrlemrALT  7381  acneq  7384  acfun  7389  tapeq1  7438  tapeq2  7439  exmidapne  7446  ccfunen  7450  cc2lem  7452  cc3  7454  ltsopi  7507  recexnq  7577  recmulnqg  7578  ltsonq  7585  lt2addnq  7591  lt2mulnq  7592  ltbtwnnqq  7602  prarloclemarch2  7606  enq0sym  7619  enq0ref  7620  enq0tr  7621  enq0breq  7623  addnq0mo  7634  mulnq0mo  7635  addnnnq0  7636  mulnnnq0  7637  nqnq0a  7641  nqnq0m  7642  elinp  7661  prcdnql  7671  prcunqu  7672  prltlu  7674  prdisj  7679  prarloclemlo  7681  prarloclem3  7684  prarloclem5  7687  ltdfpr  7693  genprndl  7708  genprndu  7709  genpdisj  7710  appdivnq  7750  ltpopr  7782  ltexprlemdisj  7793  ltexprlemloc  7794  ltexprlemrl  7797  ltexprlemru  7799  ltexpri  7800  recexprlemm  7811  recexprlemdisj  7817  recexprlemloc  7818  recexprlem1ssl  7820  recexprlem1ssu  7821  recexpr  7825  aptiprleml  7826  archpr  7830  cauappcvgprlemladdru  7843  cauappcvgprlemladdrl  7844  cauappcvgprlem1  7846  cauappcvgprlemlim  7848  cauappcvgpr  7849  caucvgprlemnkj  7853  caucvgprlemnbj  7854  caucvgprlemcl  7863  caucvgpr  7869  caucvgprprlemcbv  7874  caucvgprprlemval  7875  caucvgprprlemopu  7886  caucvgprpr  7899  suplocexpr  7912  addsrmo  7930  mulsrmo  7931  addsrpr  7932  mulsrpr  7933  lttrsr  7949  recexgt0sr  7960  caucvgsrlemcau  7980  caucvgsrlemgt1  7982  caucvgsrlemoffcau  7985  caucvgsrlemoffres  7987  caucvgsr  7989  suplocsrlem  7995  ltresr  8026  pitonn  8035  peano1nnnn  8039  peano2nnnn  8040  axprecex  8067  axcnre  8068  axpre-lttrn  8071  peano5nnnn  8079  axcaucvglemcau  8085  axcaucvglemres  8086  axpre-suploclemres  8088  axpre-suploc  8089  axlttrn  8215  axsuploc  8219  letri3  8227  letr  8229  le2add  8591  lt2add  8592  ltleadd  8593  lt2sub  8607  le2sub  8608  apreap  8734  apreim  8750  apti  8769  msq11  9049  dfinfre  9103  sup3exmid  9104  cju  9108  peano5nni  9113  1nn  9121  peano2nn  9122  nn2ge  9143  nominpos  9349  elz2  9518  dfuzi  9557  uzind  9558  supinfneg  9790  infsupneg  9791  elpqb  9845  xrletri3  10000  xrletr  10004  z2ge  10022  elixx1  10093  elioo2  10117  iooshf  10148  iooneg  10184  iccneg  10185  icoshft  10186  elfz1  10209  fzdifsuc  10277  fzrev  10280  1fv  10335  zsupcllemstep  10449  infssuzex  10453  nninfdcex  10457  zsupssdc  10458  exbtwnzlemstep  10467  exbtwnzlemshrink  10468  exbtwnzlemex  10469  exbtwnz  10470  rebtwn2zlemstep  10472  rebtwn2zlemshrink  10473  rebtwn2z  10474  qbtwnre  10476  qbtwnxr  10477  flval  10492  flqlelt  10496  flqbi  10510  flqbi2  10511  modqid2  10573  q2submod  10607  seqf1og  10743  nnesq  10881  hashunlem  11026  zfz1isolem1  11062  zfz1iso  11063  seq3coll  11064  fundm2domnop0  11067  pfxsuffeqwrdeq  11230  swrdpfx  11239  wrd2ind  11255  swrdccatin2  11261  swrdccatin2d  11276  pfxccatin12d  11277  reuccatpfxs1lem  11278  reuccatpfxs1  11279  shftlem  11327  shftfibg  11331  shftfib  11334  shftfn  11335  2shfti  11342  cjval  11356  cjth  11357  remim  11371  caucvgrelemcau  11491  caucvgre  11492  cvg1nlemcau  11495  cvg1nlemres  11496  rexanuz2  11502  recvguniq  11506  resqrexlemgt0  11531  resqrexlemoverl  11532  resqrexlemglsq  11533  resqrexlemsqa  11535  resqrexlemex  11536  rsqrmo  11538  resqrtcl  11540  rersqrtthlem  11541  absdiflt  11603  absdifle  11604  cau3lem  11625  icodiamlt  11691  maxleast  11724  negfi  11739  minmax  11741  lemininf  11745  ltmininf  11746  xrmaxlesup  11770  xrminmax  11776  xrltmininf  11781  xrlemininf  11782  iooinsup  11788  clim  11792  clim2  11794  climshftlemg  11813  addcn2  11821  climcau  11858  summodc  11894  fsum3  11898  fsum2dlemstep  11945  fisumcom2  11949  fsum00  11973  ntrivcvgap0  12060  prodeq1f  12063  prodeq2w  12067  prodeq2  12068  prodmodc  12089  zproddc  12090  fprodseq  12094  fprodntrivap  12095  fprod2dlemstep  12133  fprodcom2fi  12137  sin01bnd  12268  cos01bnd  12269  divalgmod  12438  ndvdssub  12441  gcdsupex  12478  gcdsupcl  12479  gcddvds  12484  dvdslegcd  12485  bezoutlemmain  12519  bezoutlemex  12522  bezoutlemzz  12523  bezoutlemeu  12528  bezoutlemle  12529  bezoutlemsup  12530  dfgcd3  12531  dfgcd2  12535  gcddiv  12540  lcmval  12585  lcmcllem  12589  dvdslcm  12591  lcmledvds  12592  lcmgcdlem  12599  lcmdvds  12601  coprmgcdb  12610  ncoprmgcdne1b  12611  coprmdvds1  12613  qredeu  12619  divgcdcoprm0  12623  divgcdcoprmex  12624  isprm3  12640  pw2dvdslemn  12687  pw2dvdseu  12690  oddpwdclemxy  12691  qnumdencl  12709  qnumdenbi  12714  crth  12746  reumodprminv  12776  pythagtriplem19  12805  pceu  12818  pczpre  12820  pcdiv  12825  pc11  12854  dvdsprmpweqle  12860  prmpwdvds  12878  pockthi  12881  infpnlem2  12883  elgz  12894  4sqlem12  12925  ennnfonelemim  12995  exmidunben  12997  ctinfom  12999  ctiunctlemu1st  13005  ctiunctlemu2nd  13006  ctiunctlemudc  13008  ctiunctlemfo  13010  infpn2  13027  ptex  13297  prdsval  13306  f1ocpbllem  13343  ercpbl  13364  erlecpbl  13365  grpidvalg  13406  grpidpropdg  13407  mgmlrid  13412  igsumvalx  13422  gsumfzval  13424  gsumress  13428  gsumval2  13430  issgrpd  13445  sgrppropd  13446  ismnddef  13451  sgrpidmndm  13453  ismndd  13470  mndpropd  13473  mndinvmod  13478  mnd1  13488  ismhm  13494  mhmex  13495  mhmpropd  13499  issubm  13505  insubm  13518  grppropd  13550  dfgrp2  13560  isgrpid2  13573  isgrpinv  13587  grplrinv  13590  grpidinv2  13591  grpidinv  13592  dfgrp3mlem  13631  grplactcnv  13635  releqgg  13757  eqgex  13758  eqgfval  13759  eqgval  13760  isghm  13780  ghmrn  13794  resghm  13797  ghmpropd  13820  cmnpropd  13832  ablpropd  13833  imasabl  13873  isrng  13897  rngdi  13903  rngdir  13904  rngpropd  13918  dfur2g  13925  issrg  13928  srgideu  13935  srgidmlem  13941  issrgid  13944  srg1zr  13950  isring  13963  ringideu  13980  ringidmlem  13985  isringid  13988  ringid  13989  ringpropd  14001  ring1  14022  oppr0g  14044  oppr1g  14045  dvdsrvald  14057  dvdsrd  14058  dvdsrtr  14065  unitgrp  14080  dvdsrpropdg  14111  unitpropdg  14112  rhmopp  14140  opprnzrbg  14149  opprsubrngg  14175  issubrg  14185  subrg1  14195  subrgugrp  14204  resrhm2b  14213  subrgpropd  14217  rhmpropd  14218  opprdomnbg  14238  aprval  14246  aprap  14250  islmod  14255  lmodlema  14256  islmodd  14257  lmodfopnelem2  14289  lmodprop2d  14312  islssm  14321  islssmg  14322  rnglidlrng  14462  isridl  14468  df2idl2rng  14472  quscrng  14497  istopg  14673  fiinbas  14723  eltg2  14727  topbas  14741  neiint  14819  neipsm  14828  opnneissb  14829  opnssneib  14830  innei  14837  restbasg  14842  iscnp4  14892  cnpnei  14893  cnconst2  14907  cnptopresti  14912  cnptoprest  14913  cnpdis  14916  lmss  14920  lmres  14922  txbas  14932  eltx  14933  neitx  14942  txcnp  14945  txcnmpt  14947  uptx  14948  txdis  14951  txdis1cn  14952  txlm  14953  txhmeo  14993  ispsmet  14997  ismet  15018  isxmet  15019  bldisj  15075  blininf  15098  blssexps  15103  blssex  15104  ssblex  15105  xmspropd  15151  mspropd  15152  neibl  15165  metequiv  15169  bdmopn  15178  metrest  15180  xmetxp  15181  xmetxpbl  15182  xmettx  15184  metcnp3  15185  tgioo  15228  tgqioo  15229  addcncntoplem  15235  mpomulcn  15240  mulcncflem  15281  dedekindeu  15297  dedekindicclemicc  15306  limccl  15333  ellimc3apf  15334  limcimolemlt  15338  limccoap  15352  elply2  15409  sin0pilem2  15456  sincosq1sgn  15500  sincosq2sgn  15501  sincosq3sgn  15502  sincosq4sgn  15503  perfect  15675  lgsval  15683  lgsdir2lem5  15711  lgsne0  15717  lgsquadlem1  15756  lgsquadlem2  15757  lgsquadlem3  15758  lgsquad  15759  2lgslem3  15780  2sqlem8a  15801  2sqlem8  15802  2sqlem9  15803  gropd  15848  grstructd2dom  15849  incistruhgr  15890  uhgr2edg  16004  wlkeq  16065  bj-sseq  16156  bj-charfunbi  16174  bj-nalset  16258  bj-indeq  16292  bj-2inf  16301  strcoll2  16346  strcollnft  16347  strcollnfALT  16349  sscoll2  16351  subctctexmid  16366  domomsubct  16367  exmidsbthrlem  16390  sbthom  16394  qdencn  16395  ltlenmkv  16438