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  1822  mopick  2132  clelab  2331  cbvrexfw  2729  cbvrexf  2731  cbvreu  2736  cbvrexvw  2743  cbvreuvw  2744  cbvrexdva2  2746  cbvrab  2770  gencbvex  2819  rspce  2872  eqvincf  2898  ceqsrexv  2903  elrabf  2927  rexab2  2939  reu2  2961  reu6  2962  rmo4  2966  reu8  2969  reuind  2978  sbcan  3041  sbcang  3042  sbcabel  3080  rmob  3091  cbvrexcsf  3157  cbvreucsf  3158  cbvrabcsf  3159  difjust  3167  injust  3171  eldif  3175  ssconb  3306  elin  3356  opeq1  3819  opeq2  3820  2ralunsn  3839  elunii  3855  csbunig  3858  eluniab  3862  cbvopab  4115  cbvopab1  4117  cbvopab2  4118  cbvopab1s  4119  cbvopab2v  4121  cbvmptf  4138  cbvmpt  4139  trel  4149  nalset  4174  elssabg  4192  mss  4270  exss  4271  opelopab2a  4311  poeq1  4346  pocl  4350  soeq1  4362  weeq1  4403  weeq2  4404  ordeq  4419  zfun  4481  snnex  4495  reusv3  4507  ontr2exmid  4573  regexmid  4583  onintexmid  4621  reg3exmid  4628  peano5  4646  limom  4662  nnregexmid  4669  vtoclr  4723  opeliunxp  4730  poinxp  4744  opbrop  4754  csbxpg  4756  opeliunxp2  4818  relop  4828  brcogw  4847  elrnmpt1  4929  elsnres  4996  dfres2  5011  inimasn  5100  xpcanm  5122  xpcan2m  5123  elxp4  5170  elxp5  5171  cnvsom  5226  sbcfung  5295  funopg  5305  fununi  5342  funcnvuni  5343  fneq1  5362  2elresin  5387  feq1  5408  sbcfng  5423  sbcfg  5424  f1eq1  5476  foeq1  5494  f1oeq1  5510  f1oeq2  5511  f1oeq3  5512  ffoss  5554  brprcneu  5569  fv3  5599  tz6.12f  5605  ssimaex  5640  fvopab3g  5652  fvopab3ig  5653  fvopab6  5676  fmptco  5746  funopsn  5762  funopdmsn  5764  elunirn  5835  f1imaeq  5844  foeqcnvco  5859  fliftfun  5865  fliftval  5869  isoeq1  5870  isoeq4  5873  isoini  5887  isopolem  5891  f1oiso2  5896  riotabidv  5901  cbvriota  5910  acexmid  5943  ovanraleqv  5968  cbvoprab1  6017  cbvoprab2  6018  cbvoprab12  6019  cbvmpox  6023  ov  6065  ovig  6067  ovg  6085  caovimo  6140  caoftrn  6191  opabex3d  6206  opabex3  6207  uchoice  6223  elxp6  6255  unielxp  6260  dfoprab4  6278  dfoprab4f  6279  fmpox  6286  xporderlem  6317  poxp  6318  cnvoprab  6320  f1od2  6321  opeliunxp2f  6324  rbropapd  6328  dftpos4  6349  tpostpos  6350  smoiso  6388  tfrlem3ag  6395  tfrlem3a  6396  tfr0dm  6408  tfrlemisucaccv  6411  tfrlemiex  6417  tfrlemi1  6418  tfrlemi14d  6419  tfrexlem  6420  tfr1onlem3ag  6423  tfr1onlemsucaccv  6427  tfr1onlemex  6433  tfr1onlemaccex  6434  tfr1onlemres  6435  tfrcllemsucaccv  6440  tfrcllembxssdm  6442  tfrcllemex  6446  tfrcllemaccex  6447  tfrcllemres  6448  tfrcldm  6449  frec0g  6483  frecabcl  6485  freccllem  6488  frecfcllem  6490  frecsuclem  6492  frecsuc  6493  nnacan  6598  nnmcan  6605  nnaordex  6614  ertr  6635  brecop  6712  eroveu  6713  ecopovtrn  6719  ecopovtrng  6722  th3qlem1  6724  th3qlem2  6725  th3q  6727  elpm2r  6753  mapsncnv  6782  elixp2  6789  ixpeq1  6796  elixpsn  6822  ixpsnf1o  6823  mapsnen  6903  map1  6904  xpsnen  6916  endisj  6919  pw2f1odclem  6931  xpf1o  6941  phplem3g  6953  ssfiexmid  6973  domfiexmid  6975  findcard2s  6987  isinfinf  6994  ac6sfi  6995  fiintim  7028  fisseneq  7031  opabfi  7035  f1dmvrnfibi  7046  sbthlem2  7060  isbth  7069  supeq1  7088  supeq3  7092  supeq123d  7093  supmoti  7095  eqsupti  7098  supsnti  7107  isotilem  7108  isoti  7109  supisolem  7110  supisoex  7111  cnvinfex  7120  cnvti  7121  eqinfti  7122  infvalti  7124  updjud  7184  ctssexmid  7252  omniwomnimkv  7269  exmidfodomrlemr  7310  exmidfodomrlemrALT  7311  acneq  7314  acfun  7319  tapeq1  7364  tapeq2  7365  exmidapne  7372  ccfunen  7376  cc2lem  7378  cc3  7380  ltsopi  7433  recexnq  7503  recmulnqg  7504  ltsonq  7511  lt2addnq  7517  lt2mulnq  7518  ltbtwnnqq  7528  prarloclemarch2  7532  enq0sym  7545  enq0ref  7546  enq0tr  7547  enq0breq  7549  addnq0mo  7560  mulnq0mo  7561  addnnnq0  7562  mulnnnq0  7563  nqnq0a  7567  nqnq0m  7568  elinp  7587  prcdnql  7597  prcunqu  7598  prltlu  7600  prdisj  7605  prarloclemlo  7607  prarloclem3  7610  prarloclem5  7613  ltdfpr  7619  genprndl  7634  genprndu  7635  genpdisj  7636  appdivnq  7676  ltpopr  7708  ltexprlemdisj  7719  ltexprlemloc  7720  ltexprlemrl  7723  ltexprlemru  7725  ltexpri  7726  recexprlemm  7737  recexprlemdisj  7743  recexprlemloc  7744  recexprlem1ssl  7746  recexprlem1ssu  7747  recexpr  7751  aptiprleml  7752  archpr  7756  cauappcvgprlemladdru  7769  cauappcvgprlemladdrl  7770  cauappcvgprlem1  7772  cauappcvgprlemlim  7774  cauappcvgpr  7775  caucvgprlemnkj  7779  caucvgprlemnbj  7780  caucvgprlemcl  7789  caucvgpr  7795  caucvgprprlemcbv  7800  caucvgprprlemval  7801  caucvgprprlemopu  7812  caucvgprpr  7825  suplocexpr  7838  addsrmo  7856  mulsrmo  7857  addsrpr  7858  mulsrpr  7859  lttrsr  7875  recexgt0sr  7886  caucvgsrlemcau  7906  caucvgsrlemgt1  7908  caucvgsrlemoffcau  7911  caucvgsrlemoffres  7913  caucvgsr  7915  suplocsrlem  7921  ltresr  7952  pitonn  7961  peano1nnnn  7965  peano2nnnn  7966  axprecex  7993  axcnre  7994  axpre-lttrn  7997  peano5nnnn  8005  axcaucvglemcau  8011  axcaucvglemres  8012  axpre-suploclemres  8014  axpre-suploc  8015  axlttrn  8141  axsuploc  8145  letri3  8153  letr  8155  le2add  8517  lt2add  8518  ltleadd  8519  lt2sub  8533  le2sub  8534  apreap  8660  apreim  8676  apti  8695  msq11  8975  dfinfre  9029  sup3exmid  9030  cju  9034  peano5nni  9039  1nn  9047  peano2nn  9048  nn2ge  9069  nominpos  9275  elz2  9444  dfuzi  9483  uzind  9484  supinfneg  9716  infsupneg  9717  elpqb  9771  xrletri3  9926  xrletr  9930  z2ge  9948  elixx1  10019  elioo2  10043  iooshf  10074  iooneg  10110  iccneg  10111  icoshft  10112  elfz1  10135  fzdifsuc  10203  fzrev  10206  1fv  10261  zsupcllemstep  10372  infssuzex  10376  nninfdcex  10380  zsupssdc  10381  exbtwnzlemstep  10390  exbtwnzlemshrink  10391  exbtwnzlemex  10392  exbtwnz  10393  rebtwn2zlemstep  10395  rebtwn2zlemshrink  10396  rebtwn2z  10397  qbtwnre  10399  qbtwnxr  10400  flval  10415  flqlelt  10419  flqbi  10433  flqbi2  10434  modqid2  10496  q2submod  10530  seqf1og  10666  nnesq  10804  hashunlem  10949  zfz1isolem1  10985  zfz1iso  10986  seq3coll  10987  fundm2domnop0  10990  shftlem  11127  shftfibg  11131  shftfib  11134  shftfn  11135  2shfti  11142  cjval  11156  cjth  11157  remim  11171  caucvgrelemcau  11291  caucvgre  11292  cvg1nlemcau  11295  cvg1nlemres  11296  rexanuz2  11302  recvguniq  11306  resqrexlemgt0  11331  resqrexlemoverl  11332  resqrexlemglsq  11333  resqrexlemsqa  11335  resqrexlemex  11336  rsqrmo  11338  resqrtcl  11340  rersqrtthlem  11341  absdiflt  11403  absdifle  11404  cau3lem  11425  icodiamlt  11491  maxleast  11524  negfi  11539  minmax  11541  lemininf  11545  ltmininf  11546  xrmaxlesup  11570  xrminmax  11576  xrltmininf  11581  xrlemininf  11582  iooinsup  11588  clim  11592  clim2  11594  climshftlemg  11613  addcn2  11621  climcau  11658  summodc  11694  fsum3  11698  fsum2dlemstep  11745  fisumcom2  11749  fsum00  11773  ntrivcvgap0  11860  prodeq1f  11863  prodeq2w  11867  prodeq2  11868  prodmodc  11889  zproddc  11890  fprodseq  11894  fprodntrivap  11895  fprod2dlemstep  11933  fprodcom2fi  11937  sin01bnd  12068  cos01bnd  12069  divalgmod  12238  ndvdssub  12241  gcdsupex  12278  gcdsupcl  12279  gcddvds  12284  dvdslegcd  12285  bezoutlemmain  12319  bezoutlemex  12322  bezoutlemzz  12323  bezoutlemeu  12328  bezoutlemle  12329  bezoutlemsup  12330  dfgcd3  12331  dfgcd2  12335  gcddiv  12340  lcmval  12385  lcmcllem  12389  dvdslcm  12391  lcmledvds  12392  lcmgcdlem  12399  lcmdvds  12401  coprmgcdb  12410  ncoprmgcdne1b  12411  coprmdvds1  12413  qredeu  12419  divgcdcoprm0  12423  divgcdcoprmex  12424  isprm3  12440  pw2dvdslemn  12487  pw2dvdseu  12490  oddpwdclemxy  12491  qnumdencl  12509  qnumdenbi  12514  crth  12546  reumodprminv  12576  pythagtriplem19  12605  pceu  12618  pczpre  12620  pcdiv  12625  pc11  12654  dvdsprmpweqle  12660  prmpwdvds  12678  pockthi  12681  infpnlem2  12683  elgz  12694  4sqlem12  12725  ennnfonelemim  12795  exmidunben  12797  ctinfom  12799  ctiunctlemu1st  12805  ctiunctlemu2nd  12806  ctiunctlemudc  12808  ctiunctlemfo  12810  infpn2  12827  ptex  13096  prdsval  13105  f1ocpbllem  13142  ercpbl  13163  erlecpbl  13164  grpidvalg  13205  grpidpropdg  13206  mgmlrid  13211  igsumvalx  13221  gsumfzval  13223  gsumress  13227  gsumval2  13229  issgrpd  13244  sgrppropd  13245  ismnddef  13250  sgrpidmndm  13252  ismndd  13269  mndpropd  13272  mndinvmod  13277  mnd1  13287  ismhm  13293  mhmex  13294  mhmpropd  13298  issubm  13304  insubm  13317  grppropd  13349  dfgrp2  13359  isgrpid2  13372  isgrpinv  13386  grplrinv  13389  grpidinv2  13390  grpidinv  13391  dfgrp3mlem  13430  grplactcnv  13434  releqgg  13556  eqgex  13557  eqgfval  13558  eqgval  13559  isghm  13579  ghmrn  13593  resghm  13596  ghmpropd  13619  cmnpropd  13631  ablpropd  13632  imasabl  13672  isrng  13696  rngdi  13702  rngdir  13703  rngpropd  13717  dfur2g  13724  issrg  13727  srgideu  13734  srgidmlem  13740  issrgid  13743  srg1zr  13749  isring  13762  ringideu  13779  ringidmlem  13784  isringid  13787  ringid  13788  ringpropd  13800  ring1  13821  oppr0g  13843  oppr1g  13844  reldvdsrsrg  13854  dvdsrvald  13855  dvdsrd  13856  dvdsrtr  13863  unitgrp  13878  dvdsrpropdg  13909  unitpropdg  13910  rhmopp  13938  opprnzrbg  13947  opprsubrngg  13973  issubrg  13983  subrg1  13993  subrgugrp  14002  resrhm2b  14011  subrgpropd  14015  rhmpropd  14016  opprdomnbg  14036  aprval  14044  aprap  14048  islmod  14053  lmodlema  14054  islmodd  14055  lmodfopnelem2  14087  lmodprop2d  14110  islssm  14119  islssmg  14120  rnglidlrng  14260  isridl  14266  df2idl2rng  14270  quscrng  14295  istopg  14471  fiinbas  14521  eltg2  14525  topbas  14539  neiint  14617  neipsm  14626  opnneissb  14627  opnssneib  14628  innei  14635  restbasg  14640  iscnp4  14690  cnpnei  14691  cnconst2  14705  cnptopresti  14710  cnptoprest  14711  cnpdis  14714  lmss  14718  lmres  14720  txbas  14730  eltx  14731  neitx  14740  txcnp  14743  txcnmpt  14745  uptx  14746  txdis  14749  txdis1cn  14750  txlm  14751  txhmeo  14791  ispsmet  14795  ismet  14816  isxmet  14817  bldisj  14873  blininf  14896  blssexps  14901  blssex  14902  ssblex  14903  xmspropd  14949  mspropd  14950  neibl  14963  metequiv  14967  bdmopn  14976  metrest  14978  xmetxp  14979  xmetxpbl  14980  xmettx  14982  metcnp3  14983  tgioo  15026  tgqioo  15027  addcncntoplem  15033  mpomulcn  15038  mulcncflem  15079  dedekindeu  15095  dedekindicclemicc  15104  limccl  15131  ellimc3apf  15132  limcimolemlt  15136  limccoap  15150  elply2  15207  sin0pilem2  15254  sincosq1sgn  15298  sincosq2sgn  15299  sincosq3sgn  15300  sincosq4sgn  15301  perfect  15473  lgsval  15481  lgsdir2lem5  15509  lgsne0  15515  lgsquadlem1  15554  lgsquadlem2  15555  lgsquadlem3  15556  lgsquad  15557  2lgslem3  15578  2sqlem8a  15599  2sqlem8  15600  2sqlem9  15601  gropd  15644  grstructd2dom  15645  bj-sseq  15728  bj-charfunbi  15747  bj-nalset  15831  bj-indeq  15865  bj-2inf  15874  strcoll2  15919  strcollnft  15920  strcollnfALT  15922  sscoll2  15924  subctctexmid  15937  domomsubct  15938  exmidsbthrlem  15961  sbthom  15965  qdencn  15966  ltlenmkv  16009