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  2702  cbvrexvw  2709  cbvreuvw  2710  cbvrexdva2  2712  cbvrab  2736  gencbvex  2784  rspce  2837  eqvincf  2863  ceqsrexv  2868  elrabf  2892  rexab2  2904  reu2  2926  reu6  2927  rmo4  2931  reu8  2934  reuind  2943  sbcan  3006  sbcang  3007  sbcabel  3045  rmob  3056  cbvrexcsf  3121  cbvreucsf  3122  cbvrabcsf  3123  difjust  3131  injust  3135  eldif  3139  ssconb  3269  elin  3319  opeq1  3779  opeq2  3780  2ralunsn  3799  elunii  3815  csbunig  3818  eluniab  3822  cbvopab  4075  cbvopab1  4077  cbvopab2  4078  cbvopab1s  4079  cbvopab2v  4081  cbvmptf  4098  cbvmpt  4099  trel  4109  nalset  4134  elssabg  4149  mss  4227  exss  4228  opelopab2a  4266  poeq1  4300  pocl  4304  soeq1  4316  weeq1  4357  weeq2  4358  ordeq  4373  zfun  4435  snnex  4449  reusv3  4461  ontr2exmid  4525  regexmid  4535  onintexmid  4573  reg3exmid  4580  peano5  4598  limom  4614  nnregexmid  4621  vtoclr  4675  opeliunxp  4682  poinxp  4696  opbrop  4706  csbxpg  4708  opeliunxp2  4768  relop  4778  brcogw  4797  elrnmpt1  4879  elsnres  4945  dfres2  4960  inimasn  5047  xpcanm  5069  xpcan2m  5070  elxp4  5117  elxp5  5118  cnvsom  5173  sbcfung  5241  funopg  5251  fununi  5285  funcnvuni  5286  fneq1  5305  2elresin  5328  feq1  5349  sbcfng  5364  sbcfg  5365  f1eq1  5417  foeq1  5435  f1oeq1  5450  f1oeq2  5451  f1oeq3  5452  ffoss  5494  brprcneu  5509  fv3  5539  tz6.12f  5545  ssimaex  5578  fvopab3g  5590  fvopab3ig  5591  fvopab6  5613  fmptco  5683  elunirn  5767  f1imaeq  5776  foeqcnvco  5791  fliftfun  5797  fliftval  5801  isoeq1  5802  isoeq4  5805  isoini  5819  isopolem  5823  f1oiso2  5828  riotabidv  5833  cbvriota  5841  acexmid  5874  ovanraleqv  5899  cbvoprab1  5947  cbvoprab2  5948  cbvoprab12  5949  cbvmpox  5953  ov  5994  ovig  5996  ovg  6013  caovimo  6068  caoftrn  6108  opabex3d  6122  opabex3  6123  elxp6  6170  unielxp  6175  dfoprab4  6193  dfoprab4f  6194  fmpox  6201  xporderlem  6232  poxp  6233  cnvoprab  6235  f1od2  6236  opeliunxp2f  6239  rbropapd  6243  dftpos4  6264  tpostpos  6265  smoiso  6303  tfrlem3ag  6310  tfrlem3a  6311  tfr0dm  6323  tfrlemisucaccv  6326  tfrlemiex  6332  tfrlemi1  6333  tfrlemi14d  6334  tfrexlem  6335  tfr1onlem3ag  6338  tfr1onlemsucaccv  6342  tfr1onlemex  6348  tfr1onlemaccex  6349  tfr1onlemres  6350  tfrcllemsucaccv  6355  tfrcllembxssdm  6357  tfrcllemex  6361  tfrcllemaccex  6362  tfrcllemres  6363  tfrcldm  6364  frec0g  6398  frecabcl  6400  freccllem  6403  frecfcllem  6405  frecsuclem  6407  frecsuc  6408  nnacan  6513  nnmcan  6520  nnaordex  6529  ertr  6550  brecop  6625  eroveu  6626  ecopovtrn  6632  ecopovtrng  6635  th3qlem1  6637  th3qlem2  6638  th3q  6640  elpm2r  6666  mapsncnv  6695  elixp2  6702  ixpeq1  6709  elixpsn  6735  ixpsnf1o  6736  mapsnen  6811  map1  6812  xpsnen  6821  endisj  6824  xpf1o  6844  phplem3g  6856  ssfiexmid  6876  domfiexmid  6878  findcard2s  6890  isinfinf  6897  ac6sfi  6898  fiintim  6928  fisseneq  6931  f1dmvrnfibi  6943  sbthlem2  6957  isbth  6966  supeq1  6985  supeq3  6989  supeq123d  6990  supmoti  6992  eqsupti  6995  supsnti  7004  isotilem  7005  isoti  7006  supisolem  7007  supisoex  7008  cnvinfex  7017  cnvti  7018  eqinfti  7019  infvalti  7021  updjud  7081  ctssexmid  7148  omniwomnimkv  7165  exmidfodomrlemr  7201  exmidfodomrlemrALT  7202  acfun  7206  tapeq1  7251  tapeq2  7252  exmidapne  7259  ccfunen  7263  cc2lem  7265  cc3  7267  ltsopi  7319  recexnq  7389  recmulnqg  7390  ltsonq  7397  lt2addnq  7403  lt2mulnq  7404  ltbtwnnqq  7414  prarloclemarch2  7418  enq0sym  7431  enq0ref  7432  enq0tr  7433  enq0breq  7435  addnq0mo  7446  mulnq0mo  7447  addnnnq0  7448  mulnnnq0  7449  nqnq0a  7453  nqnq0m  7454  elinp  7473  prcdnql  7483  prcunqu  7484  prltlu  7486  prdisj  7491  prarloclemlo  7493  prarloclem3  7496  prarloclem5  7499  ltdfpr  7505  genprndl  7520  genprndu  7521  genpdisj  7522  appdivnq  7562  ltpopr  7594  ltexprlemdisj  7605  ltexprlemloc  7606  ltexprlemrl  7609  ltexprlemru  7611  ltexpri  7612  recexprlemm  7623  recexprlemdisj  7629  recexprlemloc  7630  recexprlem1ssl  7632  recexprlem1ssu  7633  recexpr  7637  aptiprleml  7638  archpr  7642  cauappcvgprlemladdru  7655  cauappcvgprlemladdrl  7656  cauappcvgprlem1  7658  cauappcvgprlemlim  7660  cauappcvgpr  7661  caucvgprlemnkj  7665  caucvgprlemnbj  7666  caucvgprlemcl  7675  caucvgpr  7681  caucvgprprlemcbv  7686  caucvgprprlemval  7687  caucvgprprlemopu  7698  caucvgprpr  7711  suplocexpr  7724  addsrmo  7742  mulsrmo  7743  addsrpr  7744  mulsrpr  7745  lttrsr  7761  recexgt0sr  7772  caucvgsrlemcau  7792  caucvgsrlemgt1  7794  caucvgsrlemoffcau  7797  caucvgsrlemoffres  7799  caucvgsr  7801  suplocsrlem  7807  ltresr  7838  pitonn  7847  peano1nnnn  7851  peano2nnnn  7852  axprecex  7879  axcnre  7880  axpre-lttrn  7883  peano5nnnn  7891  axcaucvglemcau  7897  axcaucvglemres  7898  axpre-suploclemres  7900  axpre-suploc  7901  axlttrn  8026  axsuploc  8030  letri3  8038  letr  8040  le2add  8401  lt2add  8402  ltleadd  8403  lt2sub  8417  le2sub  8418  apreap  8544  apreim  8560  apti  8579  msq11  8859  dfinfre  8913  sup3exmid  8914  cju  8918  peano5nni  8922  1nn  8930  peano2nn  8931  nn2ge  8952  nominpos  9156  elz2  9324  dfuzi  9363  uzind  9364  supinfneg  9595  infsupneg  9596  elpqb  9649  xrletri3  9804  xrletr  9808  z2ge  9826  elixx1  9897  elioo2  9921  iooshf  9952  iooneg  9988  iccneg  9989  icoshft  9990  elfz1  10013  fzdifsuc  10081  fzrev  10084  1fv  10139  exbtwnzlemstep  10248  exbtwnzlemshrink  10249  exbtwnzlemex  10250  exbtwnz  10251  rebtwn2zlemstep  10253  rebtwn2zlemshrink  10254  rebtwn2z  10255  qbtwnre  10257  qbtwnxr  10258  flval  10272  flqlelt  10276  flqbi  10290  flqbi2  10291  modqid2  10351  q2submod  10385  nnesq  10640  hashunlem  10784  zfz1isolem1  10820  zfz1iso  10821  seq3coll  10822  shftlem  10825  shftfibg  10829  shftfib  10832  shftfn  10833  2shfti  10840  cjval  10854  cjth  10855  remim  10869  caucvgrelemcau  10989  caucvgre  10990  cvg1nlemcau  10993  cvg1nlemres  10994  rexanuz2  11000  recvguniq  11004  resqrexlemgt0  11029  resqrexlemoverl  11030  resqrexlemglsq  11031  resqrexlemsqa  11033  resqrexlemex  11034  rsqrmo  11036  resqrtcl  11038  rersqrtthlem  11039  absdiflt  11101  absdifle  11102  cau3lem  11123  icodiamlt  11189  maxleast  11222  negfi  11236  minmax  11238  lemininf  11242  ltmininf  11243  xrmaxlesup  11267  xrminmax  11273  xrltmininf  11278  xrlemininf  11279  iooinsup  11285  clim  11289  clim2  11291  climshftlemg  11310  addcn2  11318  climcau  11355  summodc  11391  fsum3  11395  fsum2dlemstep  11442  fisumcom2  11446  fsum00  11470  ntrivcvgap0  11557  prodeq1f  11560  prodeq2w  11564  prodeq2  11565  prodmodc  11586  zproddc  11587  fprodseq  11591  fprodntrivap  11592  fprod2dlemstep  11630  fprodcom2fi  11634  sin01bnd  11765  cos01bnd  11766  divalgmod  11932  ndvdssub  11935  zsupcllemstep  11946  infssuzex  11950  nninfdcex  11954  zsupssdc  11955  gcdsupex  11958  gcdsupcl  11959  gcddvds  11964  dvdslegcd  11965  bezoutlemmain  11999  bezoutlemex  12002  bezoutlemzz  12003  bezoutlemeu  12008  bezoutlemle  12009  bezoutlemsup  12010  dfgcd3  12011  dfgcd2  12015  gcddiv  12020  lcmval  12063  lcmcllem  12067  dvdslcm  12069  lcmledvds  12070  lcmgcdlem  12077  lcmdvds  12079  coprmgcdb  12088  ncoprmgcdne1b  12089  coprmdvds1  12091  qredeu  12097  divgcdcoprm0  12101  divgcdcoprmex  12102  isprm3  12118  pw2dvdslemn  12165  pw2dvdseu  12168  oddpwdclemxy  12169  qnumdencl  12187  qnumdenbi  12192  crth  12224  reumodprminv  12253  pythagtriplem19  12282  pceu  12295  pczpre  12297  pcdiv  12302  pc11  12330  dvdsprmpweqle  12336  prmpwdvds  12353  pockthi  12356  infpnlem2  12358  elgz  12369  ennnfonelemim  12425  exmidunben  12427  ctinfom  12429  ctiunctlemu1st  12435  ctiunctlemu2nd  12436  ctiunctlemudc  12438  ctiunctlemfo  12440  infpn2  12457  ptex  12713  f1ocpbllem  12731  ercpbl  12750  erlecpbl  12751  grpidvalg  12792  grpidpropdg  12793  mgmlrid  12798  ismnddef  12819  sgrpidmndm  12821  ismndd  12838  mndpropd  12841  mndinvmod  12846  mnd1  12847  ismhm  12853  mhmpropd  12857  issubm  12863  insubm  12872  grppropd  12893  dfgrp2  12902  isgrpid2  12913  isgrpinv  12926  grplrinv  12927  grpidinv2  12928  grpidinv  12929  dfgrp3mlem  12968  grplactcnv  12972  releqgg  13080  eqgfval  13081  eqgval  13082  cmnpropd  13098  ablpropd  13099  dfur2g  13145  issrg  13148  srgideu  13155  srgidmlem  13161  issrgid  13164  srg1zr  13170  isring  13183  ringideu  13200  ringidmlem  13205  isringid  13208  ringid  13209  ringpropd  13217  ring1  13236  oppr0g  13251  oppr1g  13252  reldvdsrsrg  13261  dvdsrvald  13262  dvdsrd  13263  dvdsrtr  13270  unitgrp  13285  dvdsrpropdg  13316  unitpropdg  13317  issubrg  13342  subrg1  13352  subrgugrp  13361  subrgpropd  13369  aprval  13372  aprap  13376  islmod  13381  lmodlema  13382  islmodd  13383  lmodfopnelem2  13415  lmodprop2d  13438  istopg  13502  fiinbas  13552  eltg2  13556  topbas  13570  neiint  13648  neipsm  13657  opnneissb  13658  opnssneib  13659  innei  13666  restbasg  13671  iscnp4  13721  cnpnei  13722  cnconst2  13736  cnptopresti  13741  cnptoprest  13742  cnpdis  13745  lmss  13749  lmres  13751  txbas  13761  eltx  13762  neitx  13771  txcnp  13774  txcnmpt  13776  uptx  13777  txdis  13780  txdis1cn  13781  txlm  13782  txhmeo  13822  ispsmet  13826  ismet  13847  isxmet  13848  bldisj  13904  blininf  13927  blssexps  13932  blssex  13933  ssblex  13934  xmspropd  13980  mspropd  13981  neibl  13994  metequiv  13998  bdmopn  14007  metrest  14009  xmetxp  14010  xmetxpbl  14011  xmettx  14013  metcnp3  14014  tgioo  14049  tgqioo  14050  addcncntoplem  14054  mulcncflem  14093  dedekindeu  14104  dedekindicclemicc  14113  limccl  14131  ellimc3apf  14132  limcimolemlt  14136  limccoap  14150  sin0pilem2  14206  sincosq1sgn  14250  sincosq2sgn  14251  sincosq3sgn  14252  sincosq4sgn  14253  lgsval  14408  lgsdir2lem5  14436  lgsne0  14442  2sqlem8a  14472  2sqlem8  14473  2sqlem9  14474  bj-sseq  14547  bj-charfunbi  14566  bj-nalset  14650  bj-indeq  14684  bj-2inf  14693  strcoll2  14738  strcollnft  14739  strcollnfALT  14741  sscoll2  14743  subctctexmid  14753  exmidsbthrlem  14773  sbthom  14777  qdencn  14778  ltlenmkv  14820