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  906  orbididc  956  3anbi123d  1325  xorbi2d  1400  xorbi1d  1401  drsb1  1823  mopick  2134  clelab  2333  cbvrmow  2691  cbvrexfw  2732  cbvrexf  2734  cbvreu  2740  cbvrexvw  2747  cbvreuvw  2748  cbvrexdva2  2750  cbvrab  2774  gencbvex  2824  rspce  2879  eqvincf  2905  ceqsrexv  2910  elrabf  2934  rexab2  2946  reu2  2968  reu6  2969  rmo4  2973  reu8  2976  reuind  2985  sbcan  3048  sbcang  3049  reu8nf  3087  sbcabel  3088  rmob  3099  cbvrexcsf  3165  cbvreucsf  3166  cbvrabcsf  3167  difjust  3175  injust  3179  eldif  3183  ssconb  3314  elin  3364  opeq1  3833  opeq2  3834  2ralunsn  3853  elunii  3869  csbunig  3872  eluniab  3876  cbvopab  4131  cbvopab1  4133  cbvopab2  4134  cbvopab1s  4135  cbvopab2v  4137  cbvmptf  4154  cbvmpt  4155  trel  4165  nalset  4190  elssabg  4208  mss  4288  exss  4289  opelopab2a  4329  poeq1  4364  pocl  4368  soeq1  4380  weeq1  4421  weeq2  4422  ordeq  4437  zfun  4499  snnex  4513  reusv3  4525  ontr2exmid  4591  regexmid  4601  onintexmid  4639  reg3exmid  4646  peano5  4664  limom  4680  nnregexmid  4687  vtoclr  4741  opeliunxp  4748  poinxp  4762  opbrop  4772  csbxpg  4774  opeliunxp2  4836  relop  4846  brcogw  4865  elrnmpt1  4948  elsnres  5015  dfres2  5030  inimasn  5119  xpcanm  5141  xpcan2m  5142  elxp4  5189  elxp5  5190  cnvsom  5245  sbcfung  5314  funopg  5324  fununi  5361  funcnvuni  5362  fneq1  5381  2elresin  5406  feq1  5428  sbcfng  5443  sbcfg  5444  f1eq1  5498  foeq1  5516  f1oeq1  5532  f1oeq2  5533  f1oeq3  5534  ffoss  5576  brprcneu  5592  fv3  5622  tz6.12f  5628  ssimaex  5663  fvopab3g  5675  fvopab3ig  5676  fvopab6  5699  fmptco  5769  funopsn  5785  funopdmsn  5787  elunirn  5858  f1imaeq  5867  foeqcnvco  5882  fliftfun  5888  fliftval  5892  isoeq1  5893  isoeq4  5896  isoini  5910  isopolem  5914  f1oiso2  5919  riotabidv  5924  cbvriota  5933  acexmid  5966  ovanraleqv  5991  cbvoprab1  6040  cbvoprab2  6041  cbvoprab12  6042  cbvmpox  6046  ov  6088  ovig  6090  ovg  6108  caovimo  6163  caoftrn  6214  opabex3d  6229  opabex3  6230  uchoice  6246  elxp6  6278  unielxp  6283  dfoprab4  6301  dfoprab4f  6302  fmpox  6309  xporderlem  6340  poxp  6341  cnvoprab  6343  f1od2  6344  opeliunxp2f  6347  rbropapd  6351  dftpos4  6372  tpostpos  6373  smoiso  6411  tfrlem3ag  6418  tfrlem3a  6419  tfr0dm  6431  tfrlemisucaccv  6434  tfrlemiex  6440  tfrlemi1  6441  tfrlemi14d  6442  tfrexlem  6443  tfr1onlem3ag  6446  tfr1onlemsucaccv  6450  tfr1onlemex  6456  tfr1onlemaccex  6457  tfr1onlemres  6458  tfrcllemsucaccv  6463  tfrcllembxssdm  6465  tfrcllemex  6469  tfrcllemaccex  6470  tfrcllemres  6471  tfrcldm  6472  frec0g  6506  frecabcl  6508  freccllem  6511  frecfcllem  6513  frecsuclem  6515  frecsuc  6516  nnacan  6621  nnmcan  6628  nnaordex  6637  ertr  6658  brecop  6735  eroveu  6736  ecopovtrn  6742  ecopovtrng  6745  th3qlem1  6747  th3qlem2  6748  th3q  6750  elpm2r  6776  mapsncnv  6805  elixp2  6812  ixpeq1  6819  elixpsn  6845  ixpsnf1o  6846  mapsnen  6927  map1  6928  xpsnen  6941  endisj  6944  pw2f1odclem  6956  xpf1o  6966  phplem3g  6978  ssfiexmid  6999  domfiexmid  7001  findcard2s  7013  isinfinf  7020  ac6sfi  7021  fiintim  7054  fisseneq  7057  opabfi  7061  f1dmvrnfibi  7072  sbthlem2  7086  isbth  7095  supeq1  7114  supeq3  7118  supeq123d  7119  supmoti  7121  eqsupti  7124  supsnti  7133  isotilem  7134  isoti  7135  supisolem  7136  supisoex  7137  cnvinfex  7146  cnvti  7147  eqinfti  7148  infvalti  7150  updjud  7210  ctssexmid  7278  omniwomnimkv  7295  exmidfodomrlemr  7341  exmidfodomrlemrALT  7342  acneq  7345  acfun  7350  tapeq1  7399  tapeq2  7400  exmidapne  7407  ccfunen  7411  cc2lem  7413  cc3  7415  ltsopi  7468  recexnq  7538  recmulnqg  7539  ltsonq  7546  lt2addnq  7552  lt2mulnq  7553  ltbtwnnqq  7563  prarloclemarch2  7567  enq0sym  7580  enq0ref  7581  enq0tr  7582  enq0breq  7584  addnq0mo  7595  mulnq0mo  7596  addnnnq0  7597  mulnnnq0  7598  nqnq0a  7602  nqnq0m  7603  elinp  7622  prcdnql  7632  prcunqu  7633  prltlu  7635  prdisj  7640  prarloclemlo  7642  prarloclem3  7645  prarloclem5  7648  ltdfpr  7654  genprndl  7669  genprndu  7670  genpdisj  7671  appdivnq  7711  ltpopr  7743  ltexprlemdisj  7754  ltexprlemloc  7755  ltexprlemrl  7758  ltexprlemru  7760  ltexpri  7761  recexprlemm  7772  recexprlemdisj  7778  recexprlemloc  7779  recexprlem1ssl  7781  recexprlem1ssu  7782  recexpr  7786  aptiprleml  7787  archpr  7791  cauappcvgprlemladdru  7804  cauappcvgprlemladdrl  7805  cauappcvgprlem1  7807  cauappcvgprlemlim  7809  cauappcvgpr  7810  caucvgprlemnkj  7814  caucvgprlemnbj  7815  caucvgprlemcl  7824  caucvgpr  7830  caucvgprprlemcbv  7835  caucvgprprlemval  7836  caucvgprprlemopu  7847  caucvgprpr  7860  suplocexpr  7873  addsrmo  7891  mulsrmo  7892  addsrpr  7893  mulsrpr  7894  lttrsr  7910  recexgt0sr  7921  caucvgsrlemcau  7941  caucvgsrlemgt1  7943  caucvgsrlemoffcau  7946  caucvgsrlemoffres  7948  caucvgsr  7950  suplocsrlem  7956  ltresr  7987  pitonn  7996  peano1nnnn  8000  peano2nnnn  8001  axprecex  8028  axcnre  8029  axpre-lttrn  8032  peano5nnnn  8040  axcaucvglemcau  8046  axcaucvglemres  8047  axpre-suploclemres  8049  axpre-suploc  8050  axlttrn  8176  axsuploc  8180  letri3  8188  letr  8190  le2add  8552  lt2add  8553  ltleadd  8554  lt2sub  8568  le2sub  8569  apreap  8695  apreim  8711  apti  8730  msq11  9010  dfinfre  9064  sup3exmid  9065  cju  9069  peano5nni  9074  1nn  9082  peano2nn  9083  nn2ge  9104  nominpos  9310  elz2  9479  dfuzi  9518  uzind  9519  supinfneg  9751  infsupneg  9752  elpqb  9806  xrletri3  9961  xrletr  9965  z2ge  9983  elixx1  10054  elioo2  10078  iooshf  10109  iooneg  10145  iccneg  10146  icoshft  10147  elfz1  10170  fzdifsuc  10238  fzrev  10241  1fv  10296  zsupcllemstep  10409  infssuzex  10413  nninfdcex  10417  zsupssdc  10418  exbtwnzlemstep  10427  exbtwnzlemshrink  10428  exbtwnzlemex  10429  exbtwnz  10430  rebtwn2zlemstep  10432  rebtwn2zlemshrink  10433  rebtwn2z  10434  qbtwnre  10436  qbtwnxr  10437  flval  10452  flqlelt  10456  flqbi  10470  flqbi2  10471  modqid2  10533  q2submod  10567  seqf1og  10703  nnesq  10841  hashunlem  10986  zfz1isolem1  11022  zfz1iso  11023  seq3coll  11024  fundm2domnop0  11027  pfxsuffeqwrdeq  11189  swrdpfx  11198  wrd2ind  11214  swrdccatin2  11220  swrdccatin2d  11235  pfxccatin12d  11236  reuccatpfxs1lem  11237  reuccatpfxs1  11238  shftlem  11242  shftfibg  11246  shftfib  11249  shftfn  11250  2shfti  11257  cjval  11271  cjth  11272  remim  11286  caucvgrelemcau  11406  caucvgre  11407  cvg1nlemcau  11410  cvg1nlemres  11411  rexanuz2  11417  recvguniq  11421  resqrexlemgt0  11446  resqrexlemoverl  11447  resqrexlemglsq  11448  resqrexlemsqa  11450  resqrexlemex  11451  rsqrmo  11453  resqrtcl  11455  rersqrtthlem  11456  absdiflt  11518  absdifle  11519  cau3lem  11540  icodiamlt  11606  maxleast  11639  negfi  11654  minmax  11656  lemininf  11660  ltmininf  11661  xrmaxlesup  11685  xrminmax  11691  xrltmininf  11696  xrlemininf  11697  iooinsup  11703  clim  11707  clim2  11709  climshftlemg  11728  addcn2  11736  climcau  11773  summodc  11809  fsum3  11813  fsum2dlemstep  11860  fisumcom2  11864  fsum00  11888  ntrivcvgap0  11975  prodeq1f  11978  prodeq2w  11982  prodeq2  11983  prodmodc  12004  zproddc  12005  fprodseq  12009  fprodntrivap  12010  fprod2dlemstep  12048  fprodcom2fi  12052  sin01bnd  12183  cos01bnd  12184  divalgmod  12353  ndvdssub  12356  gcdsupex  12393  gcdsupcl  12394  gcddvds  12399  dvdslegcd  12400  bezoutlemmain  12434  bezoutlemex  12437  bezoutlemzz  12438  bezoutlemeu  12443  bezoutlemle  12444  bezoutlemsup  12445  dfgcd3  12446  dfgcd2  12450  gcddiv  12455  lcmval  12500  lcmcllem  12504  dvdslcm  12506  lcmledvds  12507  lcmgcdlem  12514  lcmdvds  12516  coprmgcdb  12525  ncoprmgcdne1b  12526  coprmdvds1  12528  qredeu  12534  divgcdcoprm0  12538  divgcdcoprmex  12539  isprm3  12555  pw2dvdslemn  12602  pw2dvdseu  12605  oddpwdclemxy  12606  qnumdencl  12624  qnumdenbi  12629  crth  12661  reumodprminv  12691  pythagtriplem19  12720  pceu  12733  pczpre  12735  pcdiv  12740  pc11  12769  dvdsprmpweqle  12775  prmpwdvds  12793  pockthi  12796  infpnlem2  12798  elgz  12809  4sqlem12  12840  ennnfonelemim  12910  exmidunben  12912  ctinfom  12914  ctiunctlemu1st  12920  ctiunctlemu2nd  12921  ctiunctlemudc  12923  ctiunctlemfo  12925  infpn2  12942  ptex  13211  prdsval  13220  f1ocpbllem  13257  ercpbl  13278  erlecpbl  13279  grpidvalg  13320  grpidpropdg  13321  mgmlrid  13326  igsumvalx  13336  gsumfzval  13338  gsumress  13342  gsumval2  13344  issgrpd  13359  sgrppropd  13360  ismnddef  13365  sgrpidmndm  13367  ismndd  13384  mndpropd  13387  mndinvmod  13392  mnd1  13402  ismhm  13408  mhmex  13409  mhmpropd  13413  issubm  13419  insubm  13432  grppropd  13464  dfgrp2  13474  isgrpid2  13487  isgrpinv  13501  grplrinv  13504  grpidinv2  13505  grpidinv  13506  dfgrp3mlem  13545  grplactcnv  13549  releqgg  13671  eqgex  13672  eqgfval  13673  eqgval  13674  isghm  13694  ghmrn  13708  resghm  13711  ghmpropd  13734  cmnpropd  13746  ablpropd  13747  imasabl  13787  isrng  13811  rngdi  13817  rngdir  13818  rngpropd  13832  dfur2g  13839  issrg  13842  srgideu  13849  srgidmlem  13855  issrgid  13858  srg1zr  13864  isring  13877  ringideu  13894  ringidmlem  13899  isringid  13902  ringid  13903  ringpropd  13915  ring1  13936  oppr0g  13958  oppr1g  13959  reldvdsrsrg  13969  dvdsrvald  13970  dvdsrd  13971  dvdsrtr  13978  unitgrp  13993  dvdsrpropdg  14024  unitpropdg  14025  rhmopp  14053  opprnzrbg  14062  opprsubrngg  14088  issubrg  14098  subrg1  14108  subrgugrp  14117  resrhm2b  14126  subrgpropd  14130  rhmpropd  14131  opprdomnbg  14151  aprval  14159  aprap  14163  islmod  14168  lmodlema  14169  islmodd  14170  lmodfopnelem2  14202  lmodprop2d  14225  islssm  14234  islssmg  14235  rnglidlrng  14375  isridl  14381  df2idl2rng  14385  quscrng  14410  istopg  14586  fiinbas  14636  eltg2  14640  topbas  14654  neiint  14732  neipsm  14741  opnneissb  14742  opnssneib  14743  innei  14750  restbasg  14755  iscnp4  14805  cnpnei  14806  cnconst2  14820  cnptopresti  14825  cnptoprest  14826  cnpdis  14829  lmss  14833  lmres  14835  txbas  14845  eltx  14846  neitx  14855  txcnp  14858  txcnmpt  14860  uptx  14861  txdis  14864  txdis1cn  14865  txlm  14866  txhmeo  14906  ispsmet  14910  ismet  14931  isxmet  14932  bldisj  14988  blininf  15011  blssexps  15016  blssex  15017  ssblex  15018  xmspropd  15064  mspropd  15065  neibl  15078  metequiv  15082  bdmopn  15091  metrest  15093  xmetxp  15094  xmetxpbl  15095  xmettx  15097  metcnp3  15098  tgioo  15141  tgqioo  15142  addcncntoplem  15148  mpomulcn  15153  mulcncflem  15194  dedekindeu  15210  dedekindicclemicc  15219  limccl  15246  ellimc3apf  15247  limcimolemlt  15251  limccoap  15265  elply2  15322  sin0pilem2  15369  sincosq1sgn  15413  sincosq2sgn  15414  sincosq3sgn  15415  sincosq4sgn  15416  perfect  15588  lgsval  15596  lgsdir2lem5  15624  lgsne0  15630  lgsquadlem1  15669  lgsquadlem2  15670  lgsquadlem3  15671  lgsquad  15672  2lgslem3  15693  2sqlem8a  15714  2sqlem8  15715  2sqlem9  15716  gropd  15761  grstructd2dom  15762  incistruhgr  15801  bj-sseq  15928  bj-charfunbi  15946  bj-nalset  16030  bj-indeq  16064  bj-2inf  16073  strcoll2  16118  strcollnft  16119  strcollnfALT  16121  sscoll2  16123  subctctexmid  16139  domomsubct  16140  exmidsbthrlem  16163  sbthom  16167  qdencn  16168  ltlenmkv  16211