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  904  orbididc  953  3anbi123d  1312  xorbi2d  1380  xorbi1d  1381  drsb1  1799  mopick  2104  clelab  2303  cbvrexfw  2696  cbvrexf  2698  cbvreu  2703  cbvrexvw  2710  cbvreuvw  2711  cbvrexdva2  2713  cbvrab  2737  gencbvex  2785  rspce  2838  eqvincf  2864  ceqsrexv  2869  elrabf  2893  rexab2  2905  reu2  2927  reu6  2928  rmo4  2932  reu8  2935  reuind  2944  sbcan  3007  sbcang  3008  sbcabel  3046  rmob  3057  cbvrexcsf  3122  cbvreucsf  3123  cbvrabcsf  3124  difjust  3132  injust  3136  eldif  3140  ssconb  3270  elin  3320  opeq1  3780  opeq2  3781  2ralunsn  3800  elunii  3816  csbunig  3819  eluniab  3823  cbvopab  4076  cbvopab1  4078  cbvopab2  4079  cbvopab1s  4080  cbvopab2v  4082  cbvmptf  4099  cbvmpt  4100  trel  4110  nalset  4135  elssabg  4150  mss  4228  exss  4229  opelopab2a  4267  poeq1  4301  pocl  4305  soeq1  4317  weeq1  4358  weeq2  4359  ordeq  4374  zfun  4436  snnex  4450  reusv3  4462  ontr2exmid  4526  regexmid  4536  onintexmid  4574  reg3exmid  4581  peano5  4599  limom  4615  nnregexmid  4622  vtoclr  4676  opeliunxp  4683  poinxp  4697  opbrop  4707  csbxpg  4709  opeliunxp2  4769  relop  4779  brcogw  4798  elrnmpt1  4880  elsnres  4946  dfres2  4961  inimasn  5048  xpcanm  5070  xpcan2m  5071  elxp4  5118  elxp5  5119  cnvsom  5174  sbcfung  5242  funopg  5252  fununi  5286  funcnvuni  5287  fneq1  5306  2elresin  5329  feq1  5350  sbcfng  5365  sbcfg  5366  f1eq1  5418  foeq1  5436  f1oeq1  5451  f1oeq2  5452  f1oeq3  5453  ffoss  5495  brprcneu  5510  fv3  5540  tz6.12f  5546  ssimaex  5579  fvopab3g  5591  fvopab3ig  5592  fvopab6  5614  fmptco  5684  elunirn  5769  f1imaeq  5778  foeqcnvco  5793  fliftfun  5799  fliftval  5803  isoeq1  5804  isoeq4  5807  isoini  5821  isopolem  5825  f1oiso2  5830  riotabidv  5835  cbvriota  5843  acexmid  5876  ovanraleqv  5901  cbvoprab1  5949  cbvoprab2  5950  cbvoprab12  5951  cbvmpox  5955  ov  5996  ovig  5998  ovg  6015  caovimo  6070  caoftrn  6110  opabex3d  6124  opabex3  6125  elxp6  6172  unielxp  6177  dfoprab4  6195  dfoprab4f  6196  fmpox  6203  xporderlem  6234  poxp  6235  cnvoprab  6237  f1od2  6238  opeliunxp2f  6241  rbropapd  6245  dftpos4  6266  tpostpos  6267  smoiso  6305  tfrlem3ag  6312  tfrlem3a  6313  tfr0dm  6325  tfrlemisucaccv  6328  tfrlemiex  6334  tfrlemi1  6335  tfrlemi14d  6336  tfrexlem  6337  tfr1onlem3ag  6340  tfr1onlemsucaccv  6344  tfr1onlemex  6350  tfr1onlemaccex  6351  tfr1onlemres  6352  tfrcllemsucaccv  6357  tfrcllembxssdm  6359  tfrcllemex  6363  tfrcllemaccex  6364  tfrcllemres  6365  tfrcldm  6366  frec0g  6400  frecabcl  6402  freccllem  6405  frecfcllem  6407  frecsuclem  6409  frecsuc  6410  nnacan  6515  nnmcan  6522  nnaordex  6531  ertr  6552  brecop  6627  eroveu  6628  ecopovtrn  6634  ecopovtrng  6637  th3qlem1  6639  th3qlem2  6640  th3q  6642  elpm2r  6668  mapsncnv  6697  elixp2  6704  ixpeq1  6711  elixpsn  6737  ixpsnf1o  6738  mapsnen  6813  map1  6814  xpsnen  6823  endisj  6826  xpf1o  6846  phplem3g  6858  ssfiexmid  6878  domfiexmid  6880  findcard2s  6892  isinfinf  6899  ac6sfi  6900  fiintim  6930  fisseneq  6933  f1dmvrnfibi  6945  sbthlem2  6959  isbth  6968  supeq1  6987  supeq3  6991  supeq123d  6992  supmoti  6994  eqsupti  6997  supsnti  7006  isotilem  7007  isoti  7008  supisolem  7009  supisoex  7010  cnvinfex  7019  cnvti  7020  eqinfti  7021  infvalti  7023  updjud  7083  ctssexmid  7150  omniwomnimkv  7167  exmidfodomrlemr  7203  exmidfodomrlemrALT  7204  acfun  7208  tapeq1  7253  tapeq2  7254  exmidapne  7261  ccfunen  7265  cc2lem  7267  cc3  7269  ltsopi  7321  recexnq  7391  recmulnqg  7392  ltsonq  7399  lt2addnq  7405  lt2mulnq  7406  ltbtwnnqq  7416  prarloclemarch2  7420  enq0sym  7433  enq0ref  7434  enq0tr  7435  enq0breq  7437  addnq0mo  7448  mulnq0mo  7449  addnnnq0  7450  mulnnnq0  7451  nqnq0a  7455  nqnq0m  7456  elinp  7475  prcdnql  7485  prcunqu  7486  prltlu  7488  prdisj  7493  prarloclemlo  7495  prarloclem3  7498  prarloclem5  7501  ltdfpr  7507  genprndl  7522  genprndu  7523  genpdisj  7524  appdivnq  7564  ltpopr  7596  ltexprlemdisj  7607  ltexprlemloc  7608  ltexprlemrl  7611  ltexprlemru  7613  ltexpri  7614  recexprlemm  7625  recexprlemdisj  7631  recexprlemloc  7632  recexprlem1ssl  7634  recexprlem1ssu  7635  recexpr  7639  aptiprleml  7640  archpr  7644  cauappcvgprlemladdru  7657  cauappcvgprlemladdrl  7658  cauappcvgprlem1  7660  cauappcvgprlemlim  7662  cauappcvgpr  7663  caucvgprlemnkj  7667  caucvgprlemnbj  7668  caucvgprlemcl  7677  caucvgpr  7683  caucvgprprlemcbv  7688  caucvgprprlemval  7689  caucvgprprlemopu  7700  caucvgprpr  7713  suplocexpr  7726  addsrmo  7744  mulsrmo  7745  addsrpr  7746  mulsrpr  7747  lttrsr  7763  recexgt0sr  7774  caucvgsrlemcau  7794  caucvgsrlemgt1  7796  caucvgsrlemoffcau  7799  caucvgsrlemoffres  7801  caucvgsr  7803  suplocsrlem  7809  ltresr  7840  pitonn  7849  peano1nnnn  7853  peano2nnnn  7854  axprecex  7881  axcnre  7882  axpre-lttrn  7885  peano5nnnn  7893  axcaucvglemcau  7899  axcaucvglemres  7900  axpre-suploclemres  7902  axpre-suploc  7903  axlttrn  8028  axsuploc  8032  letri3  8040  letr  8042  le2add  8403  lt2add  8404  ltleadd  8405  lt2sub  8419  le2sub  8420  apreap  8546  apreim  8562  apti  8581  msq11  8861  dfinfre  8915  sup3exmid  8916  cju  8920  peano5nni  8924  1nn  8932  peano2nn  8933  nn2ge  8954  nominpos  9158  elz2  9326  dfuzi  9365  uzind  9366  supinfneg  9597  infsupneg  9598  elpqb  9651  xrletri3  9806  xrletr  9810  z2ge  9828  elixx1  9899  elioo2  9923  iooshf  9954  iooneg  9990  iccneg  9991  icoshft  9992  elfz1  10015  fzdifsuc  10083  fzrev  10086  1fv  10141  exbtwnzlemstep  10250  exbtwnzlemshrink  10251  exbtwnzlemex  10252  exbtwnz  10253  rebtwn2zlemstep  10255  rebtwn2zlemshrink  10256  rebtwn2z  10257  qbtwnre  10259  qbtwnxr  10260  flval  10274  flqlelt  10278  flqbi  10292  flqbi2  10293  modqid2  10353  q2submod  10387  nnesq  10642  hashunlem  10786  zfz1isolem1  10822  zfz1iso  10823  seq3coll  10824  shftlem  10827  shftfibg  10831  shftfib  10834  shftfn  10835  2shfti  10842  cjval  10856  cjth  10857  remim  10871  caucvgrelemcau  10991  caucvgre  10992  cvg1nlemcau  10995  cvg1nlemres  10996  rexanuz2  11002  recvguniq  11006  resqrexlemgt0  11031  resqrexlemoverl  11032  resqrexlemglsq  11033  resqrexlemsqa  11035  resqrexlemex  11036  rsqrmo  11038  resqrtcl  11040  rersqrtthlem  11041  absdiflt  11103  absdifle  11104  cau3lem  11125  icodiamlt  11191  maxleast  11224  negfi  11238  minmax  11240  lemininf  11244  ltmininf  11245  xrmaxlesup  11269  xrminmax  11275  xrltmininf  11280  xrlemininf  11281  iooinsup  11287  clim  11291  clim2  11293  climshftlemg  11312  addcn2  11320  climcau  11357  summodc  11393  fsum3  11397  fsum2dlemstep  11444  fisumcom2  11448  fsum00  11472  ntrivcvgap0  11559  prodeq1f  11562  prodeq2w  11566  prodeq2  11567  prodmodc  11588  zproddc  11589  fprodseq  11593  fprodntrivap  11594  fprod2dlemstep  11632  fprodcom2fi  11636  sin01bnd  11767  cos01bnd  11768  divalgmod  11934  ndvdssub  11937  zsupcllemstep  11948  infssuzex  11952  nninfdcex  11956  zsupssdc  11957  gcdsupex  11960  gcdsupcl  11961  gcddvds  11966  dvdslegcd  11967  bezoutlemmain  12001  bezoutlemex  12004  bezoutlemzz  12005  bezoutlemeu  12010  bezoutlemle  12011  bezoutlemsup  12012  dfgcd3  12013  dfgcd2  12017  gcddiv  12022  lcmval  12065  lcmcllem  12069  dvdslcm  12071  lcmledvds  12072  lcmgcdlem  12079  lcmdvds  12081  coprmgcdb  12090  ncoprmgcdne1b  12091  coprmdvds1  12093  qredeu  12099  divgcdcoprm0  12103  divgcdcoprmex  12104  isprm3  12120  pw2dvdslemn  12167  pw2dvdseu  12170  oddpwdclemxy  12171  qnumdencl  12189  qnumdenbi  12194  crth  12226  reumodprminv  12255  pythagtriplem19  12284  pceu  12297  pczpre  12299  pcdiv  12304  pc11  12332  dvdsprmpweqle  12338  prmpwdvds  12355  pockthi  12358  infpnlem2  12360  elgz  12371  ennnfonelemim  12427  exmidunben  12429  ctinfom  12431  ctiunctlemu1st  12437  ctiunctlemu2nd  12438  ctiunctlemudc  12440  ctiunctlemfo  12442  infpn2  12459  ptex  12718  f1ocpbllem  12736  ercpbl  12755  erlecpbl  12756  grpidvalg  12797  grpidpropdg  12798  mgmlrid  12803  ismnddef  12824  sgrpidmndm  12826  ismndd  12843  mndpropd  12846  mndinvmod  12851  mnd1  12852  ismhm  12858  mhmpropd  12862  issubm  12868  insubm  12877  grppropd  12898  dfgrp2  12907  isgrpid2  12918  isgrpinv  12931  grplrinv  12932  grpidinv2  12933  grpidinv  12934  dfgrp3mlem  12973  grplactcnv  12977  releqgg  13085  eqgfval  13086  eqgval  13087  cmnpropd  13103  ablpropd  13104  dfur2g  13150  issrg  13153  srgideu  13160  srgidmlem  13166  issrgid  13169  srg1zr  13175  isring  13188  ringideu  13205  ringidmlem  13210  isringid  13213  ringid  13214  ringpropd  13222  ring1  13241  oppr0g  13256  oppr1g  13257  reldvdsrsrg  13266  dvdsrvald  13267  dvdsrd  13268  dvdsrtr  13275  unitgrp  13290  dvdsrpropdg  13321  unitpropdg  13322  issubrg  13347  subrg1  13357  subrgugrp  13366  subrgpropd  13374  aprval  13377  aprap  13381  islmod  13386  lmodlema  13387  islmodd  13388  lmodfopnelem2  13420  lmodprop2d  13443  islssm  13450  istopg  13538  fiinbas  13588  eltg2  13592  topbas  13606  neiint  13684  neipsm  13693  opnneissb  13694  opnssneib  13695  innei  13702  restbasg  13707  iscnp4  13757  cnpnei  13758  cnconst2  13772  cnptopresti  13777  cnptoprest  13778  cnpdis  13781  lmss  13785  lmres  13787  txbas  13797  eltx  13798  neitx  13807  txcnp  13810  txcnmpt  13812  uptx  13813  txdis  13816  txdis1cn  13817  txlm  13818  txhmeo  13858  ispsmet  13862  ismet  13883  isxmet  13884  bldisj  13940  blininf  13963  blssexps  13968  blssex  13969  ssblex  13970  xmspropd  14016  mspropd  14017  neibl  14030  metequiv  14034  bdmopn  14043  metrest  14045  xmetxp  14046  xmetxpbl  14047  xmettx  14049  metcnp3  14050  tgioo  14085  tgqioo  14086  addcncntoplem  14090  mulcncflem  14129  dedekindeu  14140  dedekindicclemicc  14149  limccl  14167  ellimc3apf  14168  limcimolemlt  14172  limccoap  14186  sin0pilem2  14242  sincosq1sgn  14286  sincosq2sgn  14287  sincosq3sgn  14288  sincosq4sgn  14289  lgsval  14444  lgsdir2lem5  14472  lgsne0  14478  2sqlem8a  14508  2sqlem8  14509  2sqlem9  14510  bj-sseq  14583  bj-charfunbi  14602  bj-nalset  14686  bj-indeq  14720  bj-2inf  14729  strcoll2  14774  strcollnft  14775  strcollnfALT  14777  sscoll2  14779  subctctexmid  14789  exmidsbthrlem  14809  sbthom  14813  qdencn  14814  ltlenmkv  14857