Theorem anbi12d 465

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 461	. 2 |- ( ph -> ( ( ps /\ th ) <-> ( ch /\ th ) ) )
3		anbi12d.2	. . 3 |- ( ph -> ( th <-> ta ) )
4	3	anbi2d 460	. 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  595  pm5.17dc  894  orbididc  943  3anbi123d  1302  xorbi2d  1370  xorbi1d  1371  drsb1  1787  mopick  2092  clelab  2291  cbvrexfw  2683  cbvrexf  2685  cbvreu  2689  cbvrexvw  2696  cbvreuvw  2697  cbvrexdva2  2699  cbvrab  2723  gencbvex  2771  rspce  2824  eqvincf  2850  ceqsrexv  2855  elrabf  2879  rexab2  2891  reu2  2913  reu6  2914  rmo4  2918  reu8  2921  reuind  2930  sbcan  2992  sbcang  2993  sbcabel  3031  rmob  3042  cbvrexcsf  3107  cbvreucsf  3108  cbvrabcsf  3109  difjust  3116  injust  3120  eldif  3124  ssconb  3254  elin  3304  opeq1  3757  opeq2  3758  2ralunsn  3777  elunii  3793  csbunig  3796  eluniab  3800  cbvopab  4052  cbvopab1  4054  cbvopab2  4055  cbvopab1s  4056  cbvopab2v  4058  cbvmptf  4075  cbvmpt  4076  trel  4086  nalset  4111  elssabg  4126  mss  4203  exss  4204  opelopab2a  4242  poeq1  4276  pocl  4280  soeq1  4292  weeq1  4333  weeq2  4334  ordeq  4349  zfun  4411  snnex  4425  reusv3  4437  ontr2exmid  4501  regexmid  4511  onintexmid  4549  reg3exmid  4556  peano5  4574  limom  4590  nnregexmid  4597  vtoclr  4651  opeliunxp  4658  poinxp  4672  opbrop  4682  csbxpg  4684  opeliunxp2  4743  relop  4753  brcogw  4772  elrnmpt1  4854  elsnres  4920  dfres2  4935  inimasn  5020  xpcanm  5042  xpcan2m  5043  elxp4  5090  elxp5  5091  cnvsom  5146  sbcfung  5211  funopg  5221  fununi  5255  funcnvuni  5256  fneq1  5275  2elresin  5298  feq1  5319  sbcfng  5334  sbcfg  5335  f1eq1  5387  foeq1  5405  f1oeq1  5420  f1oeq2  5421  f1oeq3  5422  ffoss  5463  brprcneu  5478  fv3  5508  tz6.12f  5514  ssimaex  5546  fvopab3g  5558  fvopab3ig  5559  fvopab6  5581  fmptco  5650  elunirn  5733  f1imaeq  5742  foeqcnvco  5757  fliftfun  5763  fliftval  5767  isoeq1  5768  isoeq4  5771  isoini  5785  isopolem  5789  f1oiso2  5794  riotabidv  5799  cbvriota  5807  acexmid  5840  ovanraleqv  5865  cbvoprab1  5910  cbvoprab2  5911  cbvoprab12  5912  cbvmpox  5916  ov  5957  ovig  5959  ovg  5976  caovimo  6031  caoftrn  6074  opabex3d  6086  opabex3  6087  elxp6  6134  unielxp  6139  dfoprab4  6157  dfoprab4f  6158  fmpox  6165  xporderlem  6195  poxp  6196  cnvoprab  6198  f1od2  6199  opeliunxp2f  6202  rbropapd  6206  dftpos4  6227  tpostpos  6228  smoiso  6266  tfrlem3ag  6273  tfrlem3a  6274  tfr0dm  6286  tfrlemisucaccv  6289  tfrlemiex  6295  tfrlemi1  6296  tfrlemi14d  6297  tfrexlem  6298  tfr1onlem3ag  6301  tfr1onlemsucaccv  6305  tfr1onlemex  6311  tfr1onlemaccex  6312  tfr1onlemres  6313  tfrcllemsucaccv  6318  tfrcllembxssdm  6320  tfrcllemex  6324  tfrcllemaccex  6325  tfrcllemres  6326  tfrcldm  6327  frec0g  6361  frecabcl  6363  freccllem  6366  frecfcllem  6368  frecsuclem  6370  frecsuc  6371  nnacan  6476  nnmcan  6483  nnaordex  6491  ertr  6512  brecop  6587  eroveu  6588  ecopovtrn  6594  ecopovtrng  6597  th3qlem1  6599  th3qlem2  6600  th3q  6602  elpm2r  6628  mapsncnv  6657  elixp2  6664  ixpeq1  6671  elixpsn  6697  ixpsnf1o  6698  mapsnen  6773  map1  6774  xpsnen  6783  endisj  6786  xpf1o  6806  phplem3g  6818  ssfiexmid  6838  domfiexmid  6840  findcard2s  6852  isinfinf  6859  ac6sfi  6860  fiintim  6890  fisseneq  6893  f1dmvrnfibi  6905  sbthlem2  6919  isbth  6928  supeq1  6947  supeq3  6951  supeq123d  6952  supmoti  6954  eqsupti  6957  supsnti  6966  isotilem  6967  isoti  6968  supisolem  6969  supisoex  6970  cnvinfex  6979  cnvti  6980  eqinfti  6981  infvalti  6983  updjud  7043  ctssexmid  7110  omniwomnimkv  7127  exmidfodomrlemr  7154  exmidfodomrlemrALT  7155  acfun  7159  ccfunen  7201  cc2lem  7203  cc3  7205  ltsopi  7257  recexnq  7327  recmulnqg  7328  ltsonq  7335  lt2addnq  7341  lt2mulnq  7342  ltbtwnnqq  7352  prarloclemarch2  7356  enq0sym  7369  enq0ref  7370  enq0tr  7371  enq0breq  7373  addnq0mo  7384  mulnq0mo  7385  addnnnq0  7386  mulnnnq0  7387  nqnq0a  7391  nqnq0m  7392  elinp  7411  prcdnql  7421  prcunqu  7422  prltlu  7424  prdisj  7429  prarloclemlo  7431  prarloclem3  7434  prarloclem5  7437  ltdfpr  7443  genprndl  7458  genprndu  7459  genpdisj  7460  appdivnq  7500  ltpopr  7532  ltexprlemdisj  7543  ltexprlemloc  7544  ltexprlemrl  7547  ltexprlemru  7549  ltexpri  7550  recexprlemm  7561  recexprlemdisj  7567  recexprlemloc  7568  recexprlem1ssl  7570  recexprlem1ssu  7571  recexpr  7575  aptiprleml  7576  archpr  7580  cauappcvgprlemladdru  7593  cauappcvgprlemladdrl  7594  cauappcvgprlem1  7596  cauappcvgprlemlim  7598  cauappcvgpr  7599  caucvgprlemnkj  7603  caucvgprlemnbj  7604  caucvgprlemcl  7613  caucvgpr  7619  caucvgprprlemcbv  7624  caucvgprprlemval  7625  caucvgprprlemopu  7636  caucvgprpr  7649  suplocexpr  7662  addsrmo  7680  mulsrmo  7681  addsrpr  7682  mulsrpr  7683  lttrsr  7699  recexgt0sr  7710  caucvgsrlemcau  7730  caucvgsrlemgt1  7732  caucvgsrlemoffcau  7735  caucvgsrlemoffres  7737  caucvgsr  7739  suplocsrlem  7745  ltresr  7776  pitonn  7785  peano1nnnn  7789  peano2nnnn  7790  axprecex  7817  axcnre  7818  axpre-lttrn  7821  peano5nnnn  7829  axcaucvglemcau  7835  axcaucvglemres  7836  axpre-suploclemres  7838  axpre-suploc  7839  axlttrn  7963  axsuploc  7967  letri3  7975  letr  7977  le2add  8338  lt2add  8339  ltleadd  8340  lt2sub  8354  le2sub  8355  apreap  8481  apreim  8497  apti  8516  msq11  8793  dfinfre  8847  sup3exmid  8848  cju  8852  peano5nni  8856  1nn  8864  peano2nn  8865  nn2ge  8886  nominpos  9090  elz2  9258  dfuzi  9297  uzind  9298  supinfneg  9529  infsupneg  9530  elpqb  9583  xrletri3  9736  xrletr  9740  z2ge  9758  elixx1  9829  elioo2  9853  iooshf  9884  iooneg  9920  iccneg  9921  icoshft  9922  elfz1  9945  fzdifsuc  10012  fzrev  10015  1fv  10070  exbtwnzlemstep  10179  exbtwnzlemshrink  10180  exbtwnzlemex  10181  exbtwnz  10182  rebtwn2zlemstep  10184  rebtwn2zlemshrink  10185  rebtwn2z  10186  qbtwnre  10188  qbtwnxr  10189  flval  10203  flqlelt  10207  flqbi  10221  flqbi2  10222  modqid2  10282  q2submod  10316  nnesq  10570  hashunlem  10713  zfz1isolem1  10749  zfz1iso  10750  seq3coll  10751  shftlem  10754  shftfibg  10758  shftfib  10761  shftfn  10762  2shfti  10769  cjval  10783  cjth  10784  remim  10798  caucvgrelemcau  10918  caucvgre  10919  cvg1nlemcau  10922  cvg1nlemres  10923  rexanuz2  10929  recvguniq  10933  resqrexlemgt0  10958  resqrexlemoverl  10959  resqrexlemglsq  10960  resqrexlemsqa  10962  resqrexlemex  10963  rsqrmo  10965  resqrtcl  10967  rersqrtthlem  10968  absdiflt  11030  absdifle  11031  cau3lem  11052  icodiamlt  11118  maxleast  11151  negfi  11165  minmax  11167  lemininf  11171  ltmininf  11172  xrmaxlesup  11196  xrminmax  11202  xrltmininf  11207  xrlemininf  11208  iooinsup  11214  clim  11218  clim2  11220  climshftlemg  11239  addcn2  11247  climcau  11284  summodc  11320  fsum3  11324  fsum2dlemstep  11371  fisumcom2  11375  fsum00  11399  ntrivcvgap0  11486  prodeq1f  11489  prodeq2w  11493  prodeq2  11494  prodmodc  11515  zproddc  11516  fprodseq  11520  fprodntrivap  11521  fprod2dlemstep  11559  fprodcom2fi  11563  sin01bnd  11694  cos01bnd  11695  divalgmod  11860  ndvdssub  11863  zsupcllemstep  11874  infssuzex  11878  nninfdcex  11882  zsupssdc  11883  gcdsupex  11886  gcdsupcl  11887  gcddvds  11892  dvdslegcd  11893  bezoutlemmain  11927  bezoutlemex  11930  bezoutlemzz  11931  bezoutlemeu  11936  bezoutlemle  11937  bezoutlemsup  11938  dfgcd3  11939  dfgcd2  11943  gcddiv  11948  lcmval  11991  lcmcllem  11995  dvdslcm  11997  lcmledvds  11998  lcmgcdlem  12005  lcmdvds  12007  coprmgcdb  12016  ncoprmgcdne1b  12017  coprmdvds1  12019  qredeu  12025  divgcdcoprm0  12029  divgcdcoprmex  12030  isprm3  12046  pw2dvdslemn  12093  pw2dvdseu  12096  oddpwdclemxy  12097  qnumdencl  12115  qnumdenbi  12120  crth  12152  reumodprminv  12181  pythagtriplem19  12210  pceu  12223  pczpre  12225  pcdiv  12230  pc11  12258  dvdsprmpweqle  12264  prmpwdvds  12281  pockthi  12284  infpnlem2  12286  elgz  12297  ennnfonelemim  12353  exmidunben  12355  ctinfom  12357  ctiunctlemu1st  12363  ctiunctlemu2nd  12364  ctiunctlemudc  12366  ctiunctlemfo  12368  infpn2  12385  istopg  12597  fiinbas  12647  eltg2  12653  topbas  12667  neiint  12745  neipsm  12754  opnneissb  12755  opnssneib  12756  innei  12763  restbasg  12768  iscnp4  12818  cnpnei  12819  cnconst2  12833  cnptopresti  12838  cnptoprest  12839  cnpdis  12842  lmss  12846  lmres  12848  txbas  12858  eltx  12859  neitx  12868  txcnp  12871  txcnmpt  12873  uptx  12874  txdis  12877  txdis1cn  12878  txlm  12879  txhmeo  12919  ispsmet  12923  ismet  12944  isxmet  12945  bldisj  13001  blininf  13024  blssexps  13029  blssex  13030  ssblex  13031  xmspropd  13077  mspropd  13078  neibl  13091  metequiv  13095  bdmopn  13104  metrest  13106  xmetxp  13107  xmetxpbl  13108  xmettx  13110  metcnp3  13111  tgioo  13146  tgqioo  13147  addcncntoplem  13151  mulcncflem  13190  dedekindeu  13201  dedekindicclemicc  13210  limccl  13228  ellimc3apf  13229  limcimolemlt  13233  limccoap  13247  sin0pilem2  13303  sincosq1sgn  13347  sincosq2sgn  13348  sincosq3sgn  13349  sincosq4sgn  13350  lgsval  13505  lgsdir2lem5  13533  lgsne0  13539  2sqlem8a  13558  2sqlem8  13559  2sqlem9  13560  bj-sseq  13633  bj-charfunbi  13653  bj-nalset  13737  bj-indeq  13771  bj-2inf  13780  strcoll2  13825  strcollnft  13826  strcollnfALT  13828  sscoll2  13830  subctctexmid  13841  exmidsbthrlem  13861  sbthom  13865  qdencn  13866