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  5528  foeq1  5546  f1oeq1  5562  f1oeq2  5563  f1oeq3  5564  ffoss  5606  brprcneu  5622  fv3  5652  tz6.12f  5658  ssimaex  5697  fvopab3g  5709  fvopab3ig  5710  fvopab6  5733  fmptco  5803  funopsn  5819  funopdmsn  5823  elunirn  5896  f1imaeq  5905  foeqcnvco  5920  fliftfun  5926  fliftval  5930  isoeq1  5931  isoeq4  5934  isoini  5948  isopolem  5952  f1oiso2  5957  riotabidv  5962  cbvriotavw  5971  cbvriota  5972  acexmid  6006  ovanraleqv  6031  cbvoprab1  6082  cbvoprab2  6083  cbvoprab12  6084  cbvmpox  6088  ov  6130  ovig  6132  ovg  6150  caovimo  6205  caoftrn  6257  opabex3d  6272  opabex3  6273  uchoice  6289  elxp6  6321  unielxp  6326  dfoprab4  6344  dfoprab4f  6345  fmpox  6352  xporderlem  6383  poxp  6384  cnvoprab  6386  f1od2  6387  opeliunxp2f  6390  rbropapd  6394  dftpos4  6415  tpostpos  6416  smoiso  6454  tfrlem3ag  6461  tfrlem3a  6462  tfr0dm  6474  tfrlemisucaccv  6477  tfrlemiex  6483  tfrlemi1  6484  tfrlemi14d  6485  tfrexlem  6486  tfr1onlem3ag  6489  tfr1onlemsucaccv  6493  tfr1onlemex  6499  tfr1onlemaccex  6500  tfr1onlemres  6501  tfrcllemsucaccv  6506  tfrcllembxssdm  6508  tfrcllemex  6512  tfrcllemaccex  6513  tfrcllemres  6514  tfrcldm  6515  frec0g  6549  frecabcl  6551  freccllem  6554  frecfcllem  6556  frecsuclem  6558  frecsuc  6559  nnacan  6666  nnmcan  6673  nnaordex  6682  ertr  6703  brecop  6780  eroveu  6781  ecopovtrn  6787  ecopovtrng  6790  th3qlem1  6792  th3qlem2  6793  th3q  6795  elpm2r  6821  mapsncnv  6850  elixp2  6857  ixpeq1  6864  elixpsn  6890  ixpsnf1o  6891  mapsnen  6972  map1  6973  xpsnen  6988  endisj  6991  pw2f1odclem  7003  xpf1o  7013  phplem3g  7025  ssfiexmid  7046  domfiexmid  7048  findcard2s  7060  isinfinf  7067  ac6sfi  7068  fiintim  7104  fisseneq  7107  opabfi  7111  f1dmvrnfibi  7122  sbthlem2  7136  isbth  7145  supeq1  7164  supeq3  7168  supeq123d  7169  supmoti  7171  eqsupti  7174  supsnti  7183  isotilem  7184  isoti  7185  supisolem  7186  supisoex  7187  cnvinfex  7196  cnvti  7197  eqinfti  7198  infvalti  7200  updjud  7260  ctssexmid  7328  omniwomnimkv  7345  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  acneq  7395  acfun  7400  tapeq1  7449  tapeq2  7450  exmidapne  7457  ccfunen  7461  cc2lem  7463  cc3  7465  ltsopi  7518  recexnq  7588  recmulnqg  7589  ltsonq  7596  lt2addnq  7602  lt2mulnq  7603  ltbtwnnqq  7613  prarloclemarch2  7617  enq0sym  7630  enq0ref  7631  enq0tr  7632  enq0breq  7634  addnq0mo  7645  mulnq0mo  7646  addnnnq0  7647  mulnnnq0  7648  nqnq0a  7652  nqnq0m  7653  elinp  7672  prcdnql  7682  prcunqu  7683  prltlu  7685  prdisj  7690  prarloclemlo  7692  prarloclem3  7695  prarloclem5  7698  ltdfpr  7704  genprndl  7719  genprndu  7720  genpdisj  7721  appdivnq  7761  ltpopr  7793  ltexprlemdisj  7804  ltexprlemloc  7805  ltexprlemrl  7808  ltexprlemru  7810  ltexpri  7811  recexprlemm  7822  recexprlemdisj  7828  recexprlemloc  7829  recexprlem1ssl  7831  recexprlem1ssu  7832  recexpr  7836  aptiprleml  7837  archpr  7841  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  cauappcvgprlem1  7857  cauappcvgprlemlim  7859  cauappcvgpr  7860  caucvgprlemnkj  7864  caucvgprlemnbj  7865  caucvgprlemcl  7874  caucvgpr  7880  caucvgprprlemcbv  7885  caucvgprprlemval  7886  caucvgprprlemopu  7897  caucvgprpr  7910  suplocexpr  7923  addsrmo  7941  mulsrmo  7942  addsrpr  7943  mulsrpr  7944  lttrsr  7960  recexgt0sr  7971  caucvgsrlemcau  7991  caucvgsrlemgt1  7993  caucvgsrlemoffcau  7996  caucvgsrlemoffres  7998  caucvgsr  8000  suplocsrlem  8006  ltresr  8037  pitonn  8046  peano1nnnn  8050  peano2nnnn  8051  axprecex  8078  axcnre  8079  axpre-lttrn  8082  peano5nnnn  8090  axcaucvglemcau  8096  axcaucvglemres  8097  axpre-suploclemres  8099  axpre-suploc  8100  axlttrn  8226  axsuploc  8230  letri3  8238  letr  8240  le2add  8602  lt2add  8603  ltleadd  8604  lt2sub  8618  le2sub  8619  apreap  8745  apreim  8761  apti  8780  msq11  9060  dfinfre  9114  sup3exmid  9115  cju  9119  peano5nni  9124  1nn  9132  peano2nn  9133  nn2ge  9154  nominpos  9360  elz2  9529  dfuzi  9568  uzind  9569  supinfneg  9802  infsupneg  9803  elpqb  9857  xrletri3  10012  xrletr  10016  z2ge  10034  elixx1  10105  elioo2  10129  iooshf  10160  iooneg  10196  iccneg  10197  icoshft  10198  elfz1  10221  fzdifsuc  10289  fzrev  10292  1fv  10347  zsupcllemstep  10461  infssuzex  10465  nninfdcex  10469  zsupssdc  10470  exbtwnzlemstep  10479  exbtwnzlemshrink  10480  exbtwnzlemex  10481  exbtwnz  10482  rebtwn2zlemstep  10484  rebtwn2zlemshrink  10485  rebtwn2z  10486  qbtwnre  10488  qbtwnxr  10489  flval  10504  flqlelt  10508  flqbi  10522  flqbi2  10523  modqid2  10585  q2submod  10619  seqf1og  10755  nnesq  10893  hashunlem  11038  zfz1isolem1  11075  zfz1iso  11076  seq3coll  11077  fundm2domnop0  11080  pfxsuffeqwrdeq  11246  swrdpfx  11255  wrd2ind  11271  swrdccatin2  11277  swrdccatin2d  11292  pfxccatin12d  11293  reuccatpfxs1lem  11294  reuccatpfxs1  11295  shftlem  11343  shftfibg  11347  shftfib  11350  shftfn  11351  2shfti  11358  cjval  11372  cjth  11373  remim  11387  caucvgrelemcau  11507  caucvgre  11508  cvg1nlemcau  11511  cvg1nlemres  11512  rexanuz2  11518  recvguniq  11522  resqrexlemgt0  11547  resqrexlemoverl  11548  resqrexlemglsq  11549  resqrexlemsqa  11551  resqrexlemex  11552  rsqrmo  11554  resqrtcl  11556  rersqrtthlem  11557  absdiflt  11619  absdifle  11620  cau3lem  11641  icodiamlt  11707  maxleast  11740  negfi  11755  minmax  11757  lemininf  11761  ltmininf  11762  xrmaxlesup  11786  xrminmax  11792  xrltmininf  11797  xrlemininf  11798  iooinsup  11804  clim  11808  clim2  11810  climshftlemg  11829  addcn2  11837  climcau  11874  summodc  11910  fsum3  11914  fsum2dlemstep  11961  fisumcom2  11965  fsum00  11989  ntrivcvgap0  12076  prodeq1f  12079  prodeq2w  12083  prodeq2  12084  prodmodc  12105  zproddc  12106  fprodseq  12110  fprodntrivap  12111  fprod2dlemstep  12149  fprodcom2fi  12153  sin01bnd  12284  cos01bnd  12285  divalgmod  12454  ndvdssub  12457  gcdsupex  12494  gcdsupcl  12495  gcddvds  12500  dvdslegcd  12501  bezoutlemmain  12535  bezoutlemex  12538  bezoutlemzz  12539  bezoutlemeu  12544  bezoutlemle  12545  bezoutlemsup  12546  dfgcd3  12547  dfgcd2  12551  gcddiv  12556  lcmval  12601  lcmcllem  12605  dvdslcm  12607  lcmledvds  12608  lcmgcdlem  12615  lcmdvds  12617  coprmgcdb  12626  ncoprmgcdne1b  12627  coprmdvds1  12629  qredeu  12635  divgcdcoprm0  12639  divgcdcoprmex  12640  isprm3  12656  pw2dvdslemn  12703  pw2dvdseu  12706  oddpwdclemxy  12707  qnumdencl  12725  qnumdenbi  12730  crth  12762  reumodprminv  12792  pythagtriplem19  12821  pceu  12834  pczpre  12836  pcdiv  12841  pc11  12870  dvdsprmpweqle  12876  prmpwdvds  12894  pockthi  12897  infpnlem2  12899  elgz  12910  4sqlem12  12941  ennnfonelemim  13011  exmidunben  13013  ctinfom  13015  ctiunctlemu1st  13021  ctiunctlemu2nd  13022  ctiunctlemudc  13024  ctiunctlemfo  13026  infpn2  13043  ptex  13313  prdsval  13322  f1ocpbllem  13359  ercpbl  13380  erlecpbl  13381  grpidvalg  13422  grpidpropdg  13423  mgmlrid  13428  igsumvalx  13438  gsumfzval  13440  gsumress  13444  gsumval2  13446  issgrpd  13461  sgrppropd  13462  ismnddef  13467  sgrpidmndm  13469  ismndd  13486  mndpropd  13489  mndinvmod  13494  mnd1  13504  ismhm  13510  mhmex  13511  mhmpropd  13515  issubm  13521  insubm  13534  grppropd  13566  dfgrp2  13576  isgrpid2  13589  isgrpinv  13603  grplrinv  13606  grpidinv2  13607  grpidinv  13608  dfgrp3mlem  13647  grplactcnv  13651  releqgg  13773  eqgex  13774  eqgfval  13775  eqgval  13776  isghm  13796  ghmrn  13810  resghm  13813  ghmpropd  13836  cmnpropd  13848  ablpropd  13849  imasabl  13889  isrng  13913  rngdi  13919  rngdir  13920  rngpropd  13934  dfur2g  13941  issrg  13944  srgideu  13951  srgidmlem  13957  issrgid  13960  srg1zr  13966  isring  13979  ringideu  13996  ringidmlem  14001  isringid  14004  ringid  14005  ringpropd  14017  ring1  14038  oppr0g  14060  oppr1g  14061  dvdsrvald  14073  dvdsrd  14074  dvdsrtr  14081  unitgrp  14096  dvdsrpropdg  14127  unitpropdg  14128  rhmopp  14156  opprnzrbg  14165  opprsubrngg  14191  issubrg  14201  subrg1  14211  subrgugrp  14220  resrhm2b  14229  subrgpropd  14233  rhmpropd  14234  opprdomnbg  14254  aprval  14262  aprap  14266  islmod  14271  lmodlema  14272  islmodd  14273  lmodfopnelem2  14305  lmodprop2d  14328  islssm  14337  islssmg  14338  rnglidlrng  14478  isridl  14484  df2idl2rng  14488  quscrng  14513  istopg  14689  fiinbas  14739  eltg2  14743  topbas  14757  neiint  14835  neipsm  14844  opnneissb  14845  opnssneib  14846  innei  14853  restbasg  14858  iscnp4  14908  cnpnei  14909  cnconst2  14923  cnptopresti  14928  cnptoprest  14929  cnpdis  14932  lmss  14936  lmres  14938  txbas  14948  eltx  14949  neitx  14958  txcnp  14961  txcnmpt  14963  uptx  14964  txdis  14967  txdis1cn  14968  txlm  14969  txhmeo  15009  ispsmet  15013  ismet  15034  isxmet  15035  bldisj  15091  blininf  15114  blssexps  15119  blssex  15120  ssblex  15121  xmspropd  15167  mspropd  15168  neibl  15181  metequiv  15185  bdmopn  15194  metrest  15196  xmetxp  15197  xmetxpbl  15198  xmettx  15200  metcnp3  15201  tgioo  15244  tgqioo  15245  addcncntoplem  15251  mpomulcn  15256  mulcncflem  15297  dedekindeu  15313  dedekindicclemicc  15322  limccl  15349  ellimc3apf  15350  limcimolemlt  15354  limccoap  15368  elply2  15425  sin0pilem2  15472  sincosq1sgn  15516  sincosq2sgn  15517  sincosq3sgn  15518  sincosq4sgn  15519  perfect  15691  lgsval  15699  lgsdir2lem5  15727  lgsne0  15733  lgsquadlem1  15772  lgsquadlem2  15773  lgsquadlem3  15774  lgsquad  15775  2lgslem3  15796  2sqlem8a  15817  2sqlem8  15818  2sqlem9  15819  gropd  15864  grstructd2dom  15865  incistruhgr  15906  uhgr2edg  16020  vtxd0nedgbfi  16059  wlkeq  16100  istrl  16129  clwwlkn2  16163  bj-sseq  16239  bj-charfunbi  16257  bj-nalset  16341  bj-indeq  16375  bj-2inf  16384  strcoll2  16429  strcollnft  16430  strcollnfALT  16432  sscoll2  16434  subctctexmid  16453  domomsubct  16454  exmidsbthrlem  16478  sbthom  16482  qdencn  16483  ltlenmkv  16526