Theorem anbi12d 460

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 456	. 2 |- ( ph -> ( ( ps /\ th ) <-> ( ch /\ th ) ) )
3		anbi12d.2	. . 3 |- ( ph -> ( th <-> ta ) )
4	3	anbi2d 455	. 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-1 5  ax-2 6  ax-mp 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  575  pm5.17dc  854  orbididc  905  3anbi123d  1258  xorbi2d  1326  xorbi1d  1327  drsb1  1738  mopick  2038  clelab  2224  cbvrexf  2607  cbvreu  2610  cbvrexdva2  2617  cbvrab  2639  gencbvex  2687  rspce  2739  eqvincf  2764  ceqsrexv  2769  elrabf  2791  rexab2  2803  reu2  2825  reu6  2826  rmo4  2830  reu8  2833  reuind  2842  sbcan  2903  sbcang  2904  sbcabel  2942  rmob  2953  cbvrexcsf  3013  cbvreucsf  3014  cbvrabcsf  3015  difjust  3022  injust  3026  eldif  3030  ssconb  3156  elin  3206  opeq1  3652  opeq2  3653  2ralunsn  3672  elunii  3688  csbunig  3691  eluniab  3695  cbvopab  3939  cbvopab1  3941  cbvopab2  3942  cbvopab1s  3943  cbvopab2v  3945  cbvmptf  3962  cbvmpt  3963  trel  3973  nalset  3998  elssabg  4013  mss  4086  exss  4087  opelopab2a  4125  poeq1  4159  pocl  4163  soeq1  4175  weeq1  4216  weeq2  4217  ordeq  4232  zfun  4294  snnex  4307  reusv3  4319  ontr2exmid  4378  regexmid  4388  onintexmid  4425  reg3exmid  4432  peano5  4450  limom  4465  nnregexmid  4472  vtoclr  4525  opeliunxp  4532  poinxp  4546  opbrop  4556  csbxpg  4558  opeliunxp2  4617  relop  4627  brcogw  4646  elrnmpt1  4728  elsnres  4792  dfres2  4807  inimasn  4892  xpcanm  4914  xpcan2m  4915  elxp4  4962  elxp5  4963  cnvsom  5018  sbcfung  5083  funopg  5093  fununi  5127  funcnvuni  5128  fneq1  5147  2elresin  5170  feq1  5191  sbcfng  5206  sbcfg  5207  f1eq1  5259  foeq1  5277  f1oeq1  5292  f1oeq2  5293  f1oeq3  5294  ffoss  5333  brprcneu  5346  fv3  5376  tz6.12f  5382  ssimaex  5414  fvopab3g  5426  fvopab3ig  5427  fvopab6  5449  fmptco  5518  elunirn  5599  f1imaeq  5608  foeqcnvco  5623  fliftfun  5629  fliftval  5633  isoeq1  5634  isoeq4  5637  isoini  5651  isopolem  5655  f1oiso2  5660  riotabidv  5664  cbvriota  5672  acexmid  5705  ovanraleqv  5730  cbvoprab1  5775  cbvoprab2  5776  cbvoprab12  5777  cbvmpox  5781  ov  5822  ovig  5824  ovg  5841  caovimo  5896  caoftrn  5938  opabex3d  5950  opabex3  5951  elxp6  5998  unielxp  6002  dfoprab4  6020  dfoprab4f  6021  fmpox  6028  xporderlem  6058  poxp  6059  cnvoprab  6061  f1od2  6062  opeliunxp2f  6065  rbropapd  6069  dftpos4  6090  tpostpos  6091  smoiso  6129  tfrlem3ag  6136  tfrlem3a  6137  tfr0dm  6149  tfrlemisucaccv  6152  tfrlemiex  6158  tfrlemi1  6159  tfrlemi14d  6160  tfrexlem  6161  tfr1onlem3ag  6164  tfr1onlemsucaccv  6168  tfr1onlemex  6174  tfr1onlemaccex  6175  tfr1onlemres  6176  tfrcllemsucaccv  6181  tfrcllembxssdm  6183  tfrcllemex  6187  tfrcllemaccex  6188  tfrcllemres  6189  tfrcldm  6190  frec0g  6224  frecabcl  6226  freccllem  6229  frecfcllem  6231  frecsuclem  6233  frecsuc  6234  nnacan  6338  nnmcan  6345  nnaordex  6353  ertr  6374  brecop  6449  eroveu  6450  ecopovtrn  6456  ecopovtrng  6459  th3qlem1  6461  th3qlem2  6462  th3q  6464  elpm2r  6490  mapsncnv  6519  elixp2  6526  ixpeq1  6533  elixpsn  6559  ixpsnf1o  6560  mapsnen  6635  map1  6636  xpsnen  6644  endisj  6647  xpf1o  6667  phplem3g  6679  ssfiexmid  6699  domfiexmid  6701  findcard2s  6713  isinfinf  6720  ac6sfi  6721  fiintim  6746  fisseneq  6749  f1dmvrnfibi  6760  sbthlem2  6774  isbth  6783  supeq1  6788  supeq3  6792  supeq123d  6793  supmoti  6795  eqsupti  6798  supsnti  6807  isotilem  6808  isoti  6809  supisolem  6810  supisoex  6811  cnvinfex  6820  cnvti  6821  eqinfti  6822  infvalti  6824  updjud  6882  ctssexmid  6936  exmidfodomrlemr  6967  exmidfodomrlemrALT  6968  ltsopi  7029  recexnq  7099  recmulnqg  7100  ltsonq  7107  lt2addnq  7113  lt2mulnq  7114  ltbtwnnqq  7124  prarloclemarch2  7128  enq0sym  7141  enq0ref  7142  enq0tr  7143  enq0breq  7145  addnq0mo  7156  mulnq0mo  7157  addnnnq0  7158  mulnnnq0  7159  nqnq0a  7163  nqnq0m  7164  elinp  7183  prcdnql  7193  prcunqu  7194  prltlu  7196  prdisj  7201  prarloclemlo  7203  prarloclem3  7206  prarloclem5  7209  ltdfpr  7215  genprndl  7230  genprndu  7231  genpdisj  7232  appdivnq  7272  ltpopr  7304  ltexprlemdisj  7315  ltexprlemloc  7316  ltexprlemrl  7319  ltexprlemru  7321  ltexpri  7322  recexprlemm  7333  recexprlemdisj  7339  recexprlemloc  7340  recexprlem1ssl  7342  recexprlem1ssu  7343  recexpr  7347  aptiprleml  7348  archpr  7352  cauappcvgprlemladdru  7365  cauappcvgprlemladdrl  7366  cauappcvgprlem1  7368  cauappcvgprlemlim  7370  cauappcvgpr  7371  caucvgprlemnkj  7375  caucvgprlemnbj  7376  caucvgprlemcl  7385  caucvgpr  7391  caucvgprprlemcbv  7396  caucvgprprlemval  7397  caucvgprprlemopu  7408  caucvgprpr  7421  addsrmo  7439  mulsrmo  7440  addsrpr  7441  mulsrpr  7442  lttrsr  7458  recexgt0sr  7469  caucvgsrlemcau  7488  caucvgsrlemgt1  7490  caucvgsrlemoffcau  7493  caucvgsrlemoffres  7495  caucvgsr  7497  ltresr  7526  pitonn  7535  peano1nnnn  7539  peano2nnnn  7540  axprecex  7565  axcnre  7566  axpre-lttrn  7569  peano5nnnn  7577  axcaucvglemcau  7583  axcaucvglemres  7584  axlttrn  7705  letri3  7716  letr  7718  le2add  8073  lt2add  8074  ltleadd  8075  lt2sub  8089  le2sub  8090  apreap  8215  apreim  8231  apti  8250  msq11  8518  dfinfre  8572  sup3exmid  8573  cju  8577  peano5nni  8581  1nn  8589  peano2nn  8590  nn2ge  8611  nominpos  8809  elz2  8974  dfuzi  9013  uzind  9014  supinfneg  9240  infsupneg  9241  xrletri3  9429  xrletr  9432  z2ge  9450  elixx1  9521  elioo2  9545  iooshf  9576  iooneg  9612  iccneg  9613  icoshft  9614  elfz1  9636  fzdifsuc  9702  fzrev  9705  1fv  9757  exbtwnzlemstep  9866  exbtwnzlemshrink  9867  exbtwnzlemex  9868  exbtwnz  9869  rebtwn2zlemstep  9871  rebtwn2zlemshrink  9872  rebtwn2z  9873  qbtwnre  9875  qbtwnxr  9876  flval  9886  flqlelt  9890  flqbi  9904  flqbi2  9905  modqid2  9965  q2submod  9999  nnesq  10252  hashunlem  10391  zfz1isolem1  10424  zfz1iso  10425  seq3coll  10426  shftlem  10429  shftfibg  10433  shftfib  10436  shftfn  10437  2shfti  10444  cjval  10458  cjth  10459  remim  10473  caucvgrelemcau  10592  caucvgre  10593  cvg1nlemcau  10596  cvg1nlemres  10597  rexanuz2  10603  recvguniq  10607  resqrexlemgt0  10632  resqrexlemoverl  10633  resqrexlemglsq  10634  resqrexlemsqa  10636  resqrexlemex  10637  rsqrmo  10639  resqrtcl  10641  rersqrtthlem  10642  absdiflt  10704  absdifle  10705  cau3lem  10726  icodiamlt  10792  maxleast  10825  negfi  10838  minmax  10840  lemininf  10844  ltmininf  10845  xrmaxlesup  10867  xrminmax  10873  xrltmininf  10878  xrlemininf  10879  iooinsup  10885  clim  10889  clim2  10891  climshftlemg  10910  addcn2  10918  climcau  10955  summodc  10991  fsum3  10995  fsum2dlemstep  11042  fisumcom2  11046  fsum00  11070  sin01bnd  11262  cos01bnd  11263  divalgmod  11419  ndvdssub  11422  zsupcllemstep  11433  infssuzex  11437  gcdsupex  11441  gcdsupcl  11442  gcddvds  11447  dvdslegcd  11448  bezoutlemmain  11479  bezoutlemex  11482  bezoutlemzz  11483  bezoutlemeu  11488  bezoutlemle  11489  bezoutlemsup  11490  dfgcd3  11491  dfgcd2  11495  gcddiv  11500  lcmval  11537  lcmcllem  11541  dvdslcm  11543  lcmledvds  11544  lcmgcdlem  11551  lcmdvds  11553  coprmgcdb  11562  ncoprmgcdne1b  11563  coprmdvds1  11565  qredeu  11571  divgcdcoprm0  11575  divgcdcoprmex  11576  isprm3  11592  pw2dvdslemn  11635  pw2dvdseu  11638  oddpwdclemxy  11639  qnumdencl  11657  qnumdenbi  11662  crth  11692  ennnfonelemim  11729  exmidunben  11731  ctinfom  11733  istopg  11948  fiinbas  11998  eltg2  12004  topbas  12018  neiint  12096  neipsm  12105  opnneissb  12106  opnssneib  12107  innei  12114  restbasg  12119  iscnp4  12168  cnpnei  12169  cnconst2  12183  cnptopresti  12188  cnptoprest  12189  cnpdis  12192  lmss  12196  lmres  12198  txbas  12208  eltx  12209  neitx  12218  txcnp  12221  txcnmpt  12223  uptx  12224  txdis  12227  txdis1cn  12228  txlm  12229  ispsmet  12251  ismet  12272  isxmet  12273  bldisj  12329  blininf  12352  blssexps  12357  blssex  12358  ssblex  12359  xmspropd  12405  mspropd  12406  neibl  12419  metequiv  12423  bdmopn  12432  metrest  12434  metcnp3  12435  tgioo  12465  tgqioo  12466  mulcncflem  12502  limccl  12510  ellimc3ap  12511  limcimolemlt  12513  bj-sseq  12580  bj-nalset  12674  bj-indeq  12712  bj-2inf  12721  exmidsbthrlem  12801  sbthom  12805  qdencn  12806