Theorem anbi12d 470

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

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm4.38  600  pm5.17dc  899  orbididc  948  3anbi123d  1307  xorbi2d  1375  xorbi1d  1376  drsb1  1792  mopick  2097  clelab  2296  cbvrexfw  2688  cbvrexf  2690  cbvreu  2694  cbvrexvw  2701  cbvreuvw  2702  cbvrexdva2  2704  cbvrab  2728  gencbvex  2776  rspce  2829  eqvincf  2855  ceqsrexv  2860  elrabf  2884  rexab2  2896  reu2  2918  reu6  2919  rmo4  2923  reu8  2926  reuind  2935  sbcan  2997  sbcang  2998  sbcabel  3036  rmob  3047  cbvrexcsf  3112  cbvreucsf  3113  cbvrabcsf  3114  difjust  3122  injust  3126  eldif  3130  ssconb  3260  elin  3310  opeq1  3765  opeq2  3766  2ralunsn  3785  elunii  3801  csbunig  3804  eluniab  3808  cbvopab  4060  cbvopab1  4062  cbvopab2  4063  cbvopab1s  4064  cbvopab2v  4066  cbvmptf  4083  cbvmpt  4084  trel  4094  nalset  4119  elssabg  4134  mss  4211  exss  4212  opelopab2a  4250  poeq1  4284  pocl  4288  soeq1  4300  weeq1  4341  weeq2  4342  ordeq  4357  zfun  4419  snnex  4433  reusv3  4445  ontr2exmid  4509  regexmid  4519  onintexmid  4557  reg3exmid  4564  peano5  4582  limom  4598  nnregexmid  4605  vtoclr  4659  opeliunxp  4666  poinxp  4680  opbrop  4690  csbxpg  4692  opeliunxp2  4751  relop  4761  brcogw  4780  elrnmpt1  4862  elsnres  4928  dfres2  4943  inimasn  5028  xpcanm  5050  xpcan2m  5051  elxp4  5098  elxp5  5099  cnvsom  5154  sbcfung  5222  funopg  5232  fununi  5266  funcnvuni  5267  fneq1  5286  2elresin  5309  feq1  5330  sbcfng  5345  sbcfg  5346  f1eq1  5398  foeq1  5416  f1oeq1  5431  f1oeq2  5432  f1oeq3  5433  ffoss  5474  brprcneu  5489  fv3  5519  tz6.12f  5525  ssimaex  5557  fvopab3g  5569  fvopab3ig  5570  fvopab6  5592  fmptco  5662  elunirn  5745  f1imaeq  5754  foeqcnvco  5769  fliftfun  5775  fliftval  5779  isoeq1  5780  isoeq4  5783  isoini  5797  isopolem  5801  f1oiso2  5806  riotabidv  5811  cbvriota  5819  acexmid  5852  ovanraleqv  5877  cbvoprab1  5925  cbvoprab2  5926  cbvoprab12  5927  cbvmpox  5931  ov  5972  ovig  5974  ovg  5991  caovimo  6046  caoftrn  6086  opabex3d  6100  opabex3  6101  elxp6  6148  unielxp  6153  dfoprab4  6171  dfoprab4f  6172  fmpox  6179  xporderlem  6210  poxp  6211  cnvoprab  6213  f1od2  6214  opeliunxp2f  6217  rbropapd  6221  dftpos4  6242  tpostpos  6243  smoiso  6281  tfrlem3ag  6288  tfrlem3a  6289  tfr0dm  6301  tfrlemisucaccv  6304  tfrlemiex  6310  tfrlemi1  6311  tfrlemi14d  6312  tfrexlem  6313  tfr1onlem3ag  6316  tfr1onlemsucaccv  6320  tfr1onlemex  6326  tfr1onlemaccex  6327  tfr1onlemres  6328  tfrcllemsucaccv  6333  tfrcllembxssdm  6335  tfrcllemex  6339  tfrcllemaccex  6340  tfrcllemres  6341  tfrcldm  6342  frec0g  6376  frecabcl  6378  freccllem  6381  frecfcllem  6383  frecsuclem  6385  frecsuc  6386  nnacan  6491  nnmcan  6498  nnaordex  6507  ertr  6528  brecop  6603  eroveu  6604  ecopovtrn  6610  ecopovtrng  6613  th3qlem1  6615  th3qlem2  6616  th3q  6618  elpm2r  6644  mapsncnv  6673  elixp2  6680  ixpeq1  6687  elixpsn  6713  ixpsnf1o  6714  mapsnen  6789  map1  6790  xpsnen  6799  endisj  6802  xpf1o  6822  phplem3g  6834  ssfiexmid  6854  domfiexmid  6856  findcard2s  6868  isinfinf  6875  ac6sfi  6876  fiintim  6906  fisseneq  6909  f1dmvrnfibi  6921  sbthlem2  6935  isbth  6944  supeq1  6963  supeq3  6967  supeq123d  6968  supmoti  6970  eqsupti  6973  supsnti  6982  isotilem  6983  isoti  6984  supisolem  6985  supisoex  6986  cnvinfex  6995  cnvti  6996  eqinfti  6997  infvalti  6999  updjud  7059  ctssexmid  7126  omniwomnimkv  7143  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  acfun  7184  ccfunen  7226  cc2lem  7228  cc3  7230  ltsopi  7282  recexnq  7352  recmulnqg  7353  ltsonq  7360  lt2addnq  7366  lt2mulnq  7367  ltbtwnnqq  7377  prarloclemarch2  7381  enq0sym  7394  enq0ref  7395  enq0tr  7396  enq0breq  7398  addnq0mo  7409  mulnq0mo  7410  addnnnq0  7411  mulnnnq0  7412  nqnq0a  7416  nqnq0m  7417  elinp  7436  prcdnql  7446  prcunqu  7447  prltlu  7449  prdisj  7454  prarloclemlo  7456  prarloclem3  7459  prarloclem5  7462  ltdfpr  7468  genprndl  7483  genprndu  7484  genpdisj  7485  appdivnq  7525  ltpopr  7557  ltexprlemdisj  7568  ltexprlemloc  7569  ltexprlemrl  7572  ltexprlemru  7574  ltexpri  7575  recexprlemm  7586  recexprlemdisj  7592  recexprlemloc  7593  recexprlem1ssl  7595  recexprlem1ssu  7596  recexpr  7600  aptiprleml  7601  archpr  7605  cauappcvgprlemladdru  7618  cauappcvgprlemladdrl  7619  cauappcvgprlem1  7621  cauappcvgprlemlim  7623  cauappcvgpr  7624  caucvgprlemnkj  7628  caucvgprlemnbj  7629  caucvgprlemcl  7638  caucvgpr  7644  caucvgprprlemcbv  7649  caucvgprprlemval  7650  caucvgprprlemopu  7661  caucvgprpr  7674  suplocexpr  7687  addsrmo  7705  mulsrmo  7706  addsrpr  7707  mulsrpr  7708  lttrsr  7724  recexgt0sr  7735  caucvgsrlemcau  7755  caucvgsrlemgt1  7757  caucvgsrlemoffcau  7760  caucvgsrlemoffres  7762  caucvgsr  7764  suplocsrlem  7770  ltresr  7801  pitonn  7810  peano1nnnn  7814  peano2nnnn  7815  axprecex  7842  axcnre  7843  axpre-lttrn  7846  peano5nnnn  7854  axcaucvglemcau  7860  axcaucvglemres  7861  axpre-suploclemres  7863  axpre-suploc  7864  axlttrn  7988  axsuploc  7992  letri3  8000  letr  8002  le2add  8363  lt2add  8364  ltleadd  8365  lt2sub  8379  le2sub  8380  apreap  8506  apreim  8522  apti  8541  msq11  8818  dfinfre  8872  sup3exmid  8873  cju  8877  peano5nni  8881  1nn  8889  peano2nn  8890  nn2ge  8911  nominpos  9115  elz2  9283  dfuzi  9322  uzind  9323  supinfneg  9554  infsupneg  9555  elpqb  9608  xrletri3  9761  xrletr  9765  z2ge  9783  elixx1  9854  elioo2  9878  iooshf  9909  iooneg  9945  iccneg  9946  icoshft  9947  elfz1  9970  fzdifsuc  10037  fzrev  10040  1fv  10095  exbtwnzlemstep  10204  exbtwnzlemshrink  10205  exbtwnzlemex  10206  exbtwnz  10207  rebtwn2zlemstep  10209  rebtwn2zlemshrink  10210  rebtwn2z  10211  qbtwnre  10213  qbtwnxr  10214  flval  10228  flqlelt  10232  flqbi  10246  flqbi2  10247  modqid2  10307  q2submod  10341  nnesq  10595  hashunlem  10739  zfz1isolem1  10775  zfz1iso  10776  seq3coll  10777  shftlem  10780  shftfibg  10784  shftfib  10787  shftfn  10788  2shfti  10795  cjval  10809  cjth  10810  remim  10824  caucvgrelemcau  10944  caucvgre  10945  cvg1nlemcau  10948  cvg1nlemres  10949  rexanuz2  10955  recvguniq  10959  resqrexlemgt0  10984  resqrexlemoverl  10985  resqrexlemglsq  10986  resqrexlemsqa  10988  resqrexlemex  10989  rsqrmo  10991  resqrtcl  10993  rersqrtthlem  10994  absdiflt  11056  absdifle  11057  cau3lem  11078  icodiamlt  11144  maxleast  11177  negfi  11191  minmax  11193  lemininf  11197  ltmininf  11198  xrmaxlesup  11222  xrminmax  11228  xrltmininf  11233  xrlemininf  11234  iooinsup  11240  clim  11244  clim2  11246  climshftlemg  11265  addcn2  11273  climcau  11310  summodc  11346  fsum3  11350  fsum2dlemstep  11397  fisumcom2  11401  fsum00  11425  ntrivcvgap0  11512  prodeq1f  11515  prodeq2w  11519  prodeq2  11520  prodmodc  11541  zproddc  11542  fprodseq  11546  fprodntrivap  11547  fprod2dlemstep  11585  fprodcom2fi  11589  sin01bnd  11720  cos01bnd  11721  divalgmod  11886  ndvdssub  11889  zsupcllemstep  11900  infssuzex  11904  nninfdcex  11908  zsupssdc  11909  gcdsupex  11912  gcdsupcl  11913  gcddvds  11918  dvdslegcd  11919  bezoutlemmain  11953  bezoutlemex  11956  bezoutlemzz  11957  bezoutlemeu  11962  bezoutlemle  11963  bezoutlemsup  11964  dfgcd3  11965  dfgcd2  11969  gcddiv  11974  lcmval  12017  lcmcllem  12021  dvdslcm  12023  lcmledvds  12024  lcmgcdlem  12031  lcmdvds  12033  coprmgcdb  12042  ncoprmgcdne1b  12043  coprmdvds1  12045  qredeu  12051  divgcdcoprm0  12055  divgcdcoprmex  12056  isprm3  12072  pw2dvdslemn  12119  pw2dvdseu  12122  oddpwdclemxy  12123  qnumdencl  12141  qnumdenbi  12146  crth  12178  reumodprminv  12207  pythagtriplem19  12236  pceu  12249  pczpre  12251  pcdiv  12256  pc11  12284  dvdsprmpweqle  12290  prmpwdvds  12307  pockthi  12310  infpnlem2  12312  elgz  12323  ennnfonelemim  12379  exmidunben  12381  ctinfom  12383  ctiunctlemu1st  12389  ctiunctlemu2nd  12390  ctiunctlemudc  12392  ctiunctlemfo  12394  infpn2  12411  grpidvalg  12627  grpidpropdg  12628  mgmlrid  12633  ismnddef  12654  sgrpidmndm  12656  ismndd  12673  mndpropd  12676  mndinvmod  12678  mnd1  12679  ismhm  12685  mhmpropd  12689  issubm  12695  insubm  12703  grppropd  12724  dfgrp2  12732  isgrpid2  12743  isgrpinv  12756  grplrinv  12757  grpidinv2  12758  grpidinv  12759  istopg  12791  fiinbas  12841  eltg2  12847  topbas  12861  neiint  12939  neipsm  12948  opnneissb  12949  opnssneib  12950  innei  12957  restbasg  12962  iscnp4  13012  cnpnei  13013  cnconst2  13027  cnptopresti  13032  cnptoprest  13033  cnpdis  13036  lmss  13040  lmres  13042  txbas  13052  eltx  13053  neitx  13062  txcnp  13065  txcnmpt  13067  uptx  13068  txdis  13071  txdis1cn  13072  txlm  13073  txhmeo  13113  ispsmet  13117  ismet  13138  isxmet  13139  bldisj  13195  blininf  13218  blssexps  13223  blssex  13224  ssblex  13225  xmspropd  13271  mspropd  13272  neibl  13285  metequiv  13289  bdmopn  13298  metrest  13300  xmetxp  13301  xmetxpbl  13302  xmettx  13304  metcnp3  13305  tgioo  13340  tgqioo  13341  addcncntoplem  13345  mulcncflem  13384  dedekindeu  13395  dedekindicclemicc  13404  limccl  13422  ellimc3apf  13423  limcimolemlt  13427  limccoap  13441  sin0pilem2  13497  sincosq1sgn  13541  sincosq2sgn  13542  sincosq3sgn  13543  sincosq4sgn  13544  lgsval  13699  lgsdir2lem5  13727  lgsne0  13733  2sqlem8a  13752  2sqlem8  13753  2sqlem9  13754  bj-sseq  13827  bj-charfunbi  13846  bj-nalset  13930  bj-indeq  13964  bj-2inf  13973  strcoll2  14018  strcollnft  14019  strcollnfALT  14021  sscoll2  14023  subctctexmid  14034  exmidsbthrlem  14054  sbthom  14058  qdencn  14059