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  905  orbididc  955  3anbi123d  1323  xorbi2d  1391  xorbi1d  1392  drsb1  1810  mopick  2116  clelab  2315  cbvrexfw  2709  cbvrexf  2711  cbvreu  2716  cbvrexvw  2723  cbvreuvw  2724  cbvrexdva2  2726  cbvrab  2750  gencbvex  2798  rspce  2851  eqvincf  2877  ceqsrexv  2882  elrabf  2906  rexab2  2918  reu2  2940  reu6  2941  rmo4  2945  reu8  2948  reuind  2957  sbcan  3020  sbcang  3021  sbcabel  3059  rmob  3070  cbvrexcsf  3135  cbvreucsf  3136  cbvrabcsf  3137  difjust  3145  injust  3149  eldif  3153  ssconb  3283  elin  3333  opeq1  3793  opeq2  3794  2ralunsn  3813  elunii  3829  csbunig  3832  eluniab  3836  cbvopab  4089  cbvopab1  4091  cbvopab2  4092  cbvopab1s  4093  cbvopab2v  4095  cbvmptf  4112  cbvmpt  4113  trel  4123  nalset  4148  elssabg  4163  mss  4241  exss  4242  opelopab2a  4280  poeq1  4314  pocl  4318  soeq1  4330  weeq1  4371  weeq2  4372  ordeq  4387  zfun  4449  snnex  4463  reusv3  4475  ontr2exmid  4539  regexmid  4549  onintexmid  4587  reg3exmid  4594  peano5  4612  limom  4628  nnregexmid  4635  vtoclr  4689  opeliunxp  4696  poinxp  4710  opbrop  4720  csbxpg  4722  opeliunxp2  4782  relop  4792  brcogw  4811  elrnmpt1  4893  elsnres  4959  dfres2  4974  inimasn  5061  xpcanm  5083  xpcan2m  5084  elxp4  5131  elxp5  5132  cnvsom  5187  sbcfung  5256  funopg  5266  fununi  5300  funcnvuni  5301  fneq1  5320  2elresin  5343  feq1  5364  sbcfng  5379  sbcfg  5380  f1eq1  5432  foeq1  5450  f1oeq1  5465  f1oeq2  5466  f1oeq3  5467  ffoss  5509  brprcneu  5524  fv3  5554  tz6.12f  5560  ssimaex  5594  fvopab3g  5606  fvopab3ig  5607  fvopab6  5629  fmptco  5699  elunirn  5784  f1imaeq  5793  foeqcnvco  5808  fliftfun  5814  fliftval  5818  isoeq1  5819  isoeq4  5822  isoini  5836  isopolem  5840  f1oiso2  5845  riotabidv  5850  cbvriota  5858  acexmid  5891  ovanraleqv  5916  cbvoprab1  5964  cbvoprab2  5965  cbvoprab12  5966  cbvmpox  5970  ov  6012  ovig  6014  ovg  6031  caovimo  6086  caoftrn  6127  opabex3d  6141  opabex3  6142  elxp6  6189  unielxp  6194  dfoprab4  6212  dfoprab4f  6213  fmpox  6220  xporderlem  6251  poxp  6252  cnvoprab  6254  f1od2  6255  opeliunxp2f  6258  rbropapd  6262  dftpos4  6283  tpostpos  6284  smoiso  6322  tfrlem3ag  6329  tfrlem3a  6330  tfr0dm  6342  tfrlemisucaccv  6345  tfrlemiex  6351  tfrlemi1  6352  tfrlemi14d  6353  tfrexlem  6354  tfr1onlem3ag  6357  tfr1onlemsucaccv  6361  tfr1onlemex  6367  tfr1onlemaccex  6368  tfr1onlemres  6369  tfrcllemsucaccv  6374  tfrcllembxssdm  6376  tfrcllemex  6380  tfrcllemaccex  6381  tfrcllemres  6382  tfrcldm  6383  frec0g  6417  frecabcl  6419  freccllem  6422  frecfcllem  6424  frecsuclem  6426  frecsuc  6427  nnacan  6532  nnmcan  6539  nnaordex  6548  ertr  6569  brecop  6646  eroveu  6647  ecopovtrn  6653  ecopovtrng  6656  th3qlem1  6658  th3qlem2  6659  th3q  6661  elpm2r  6687  mapsncnv  6716  elixp2  6723  ixpeq1  6730  elixpsn  6756  ixpsnf1o  6757  mapsnen  6832  map1  6833  xpsnen  6842  endisj  6845  pw2f1odclem  6857  xpf1o  6867  phplem3g  6879  ssfiexmid  6899  domfiexmid  6901  findcard2s  6913  isinfinf  6920  ac6sfi  6921  fiintim  6952  fisseneq  6955  f1dmvrnfibi  6968  sbthlem2  6982  isbth  6991  supeq1  7010  supeq3  7014  supeq123d  7015  supmoti  7017  eqsupti  7020  supsnti  7029  isotilem  7030  isoti  7031  supisolem  7032  supisoex  7033  cnvinfex  7042  cnvti  7043  eqinfti  7044  infvalti  7046  updjud  7106  ctssexmid  7173  omniwomnimkv  7190  exmidfodomrlemr  7226  exmidfodomrlemrALT  7227  acfun  7231  tapeq1  7276  tapeq2  7277  exmidapne  7284  ccfunen  7288  cc2lem  7290  cc3  7292  ltsopi  7344  recexnq  7414  recmulnqg  7415  ltsonq  7422  lt2addnq  7428  lt2mulnq  7429  ltbtwnnqq  7439  prarloclemarch2  7443  enq0sym  7456  enq0ref  7457  enq0tr  7458  enq0breq  7460  addnq0mo  7471  mulnq0mo  7472  addnnnq0  7473  mulnnnq0  7474  nqnq0a  7478  nqnq0m  7479  elinp  7498  prcdnql  7508  prcunqu  7509  prltlu  7511  prdisj  7516  prarloclemlo  7518  prarloclem3  7521  prarloclem5  7524  ltdfpr  7530  genprndl  7545  genprndu  7546  genpdisj  7547  appdivnq  7587  ltpopr  7619  ltexprlemdisj  7630  ltexprlemloc  7631  ltexprlemrl  7634  ltexprlemru  7636  ltexpri  7637  recexprlemm  7648  recexprlemdisj  7654  recexprlemloc  7655  recexprlem1ssl  7657  recexprlem1ssu  7658  recexpr  7662  aptiprleml  7663  archpr  7667  cauappcvgprlemladdru  7680  cauappcvgprlemladdrl  7681  cauappcvgprlem1  7683  cauappcvgprlemlim  7685  cauappcvgpr  7686  caucvgprlemnkj  7690  caucvgprlemnbj  7691  caucvgprlemcl  7700  caucvgpr  7706  caucvgprprlemcbv  7711  caucvgprprlemval  7712  caucvgprprlemopu  7723  caucvgprpr  7736  suplocexpr  7749  addsrmo  7767  mulsrmo  7768  addsrpr  7769  mulsrpr  7770  lttrsr  7786  recexgt0sr  7797  caucvgsrlemcau  7817  caucvgsrlemgt1  7819  caucvgsrlemoffcau  7822  caucvgsrlemoffres  7824  caucvgsr  7826  suplocsrlem  7832  ltresr  7863  pitonn  7872  peano1nnnn  7876  peano2nnnn  7877  axprecex  7904  axcnre  7905  axpre-lttrn  7908  peano5nnnn  7916  axcaucvglemcau  7922  axcaucvglemres  7923  axpre-suploclemres  7925  axpre-suploc  7926  axlttrn  8051  axsuploc  8055  letri3  8063  letr  8065  le2add  8426  lt2add  8427  ltleadd  8428  lt2sub  8442  le2sub  8443  apreap  8569  apreim  8585  apti  8604  msq11  8884  dfinfre  8938  sup3exmid  8939  cju  8943  peano5nni  8947  1nn  8955  peano2nn  8956  nn2ge  8977  nominpos  9181  elz2  9349  dfuzi  9388  uzind  9389  supinfneg  9620  infsupneg  9621  elpqb  9674  xrletri3  9829  xrletr  9833  z2ge  9851  elixx1  9922  elioo2  9946  iooshf  9977  iooneg  10013  iccneg  10014  icoshft  10015  elfz1  10038  fzdifsuc  10106  fzrev  10109  1fv  10164  exbtwnzlemstep  10273  exbtwnzlemshrink  10274  exbtwnzlemex  10275  exbtwnz  10276  rebtwn2zlemstep  10278  rebtwn2zlemshrink  10279  rebtwn2z  10280  qbtwnre  10282  qbtwnxr  10283  flval  10298  flqlelt  10302  flqbi  10316  flqbi2  10317  modqid2  10377  q2submod  10411  nnesq  10666  hashunlem  10811  zfz1isolem1  10847  zfz1iso  10848  seq3coll  10849  shftlem  10852  shftfibg  10856  shftfib  10859  shftfn  10860  2shfti  10867  cjval  10881  cjth  10882  remim  10896  caucvgrelemcau  11016  caucvgre  11017  cvg1nlemcau  11020  cvg1nlemres  11021  rexanuz2  11027  recvguniq  11031  resqrexlemgt0  11056  resqrexlemoverl  11057  resqrexlemglsq  11058  resqrexlemsqa  11060  resqrexlemex  11061  rsqrmo  11063  resqrtcl  11065  rersqrtthlem  11066  absdiflt  11128  absdifle  11129  cau3lem  11150  icodiamlt  11216  maxleast  11249  negfi  11263  minmax  11265  lemininf  11269  ltmininf  11270  xrmaxlesup  11294  xrminmax  11300  xrltmininf  11305  xrlemininf  11306  iooinsup  11312  clim  11316  clim2  11318  climshftlemg  11337  addcn2  11345  climcau  11382  summodc  11418  fsum3  11422  fsum2dlemstep  11469  fisumcom2  11473  fsum00  11497  ntrivcvgap0  11584  prodeq1f  11587  prodeq2w  11591  prodeq2  11592  prodmodc  11613  zproddc  11614  fprodseq  11618  fprodntrivap  11619  fprod2dlemstep  11657  fprodcom2fi  11661  sin01bnd  11792  cos01bnd  11793  divalgmod  11959  ndvdssub  11962  zsupcllemstep  11973  infssuzex  11977  nninfdcex  11981  zsupssdc  11982  gcdsupex  11985  gcdsupcl  11986  gcddvds  11991  dvdslegcd  11992  bezoutlemmain  12026  bezoutlemex  12029  bezoutlemzz  12030  bezoutlemeu  12035  bezoutlemle  12036  bezoutlemsup  12037  dfgcd3  12038  dfgcd2  12042  gcddiv  12047  lcmval  12090  lcmcllem  12094  dvdslcm  12096  lcmledvds  12097  lcmgcdlem  12104  lcmdvds  12106  coprmgcdb  12115  ncoprmgcdne1b  12116  coprmdvds1  12118  qredeu  12124  divgcdcoprm0  12128  divgcdcoprmex  12129  isprm3  12145  pw2dvdslemn  12192  pw2dvdseu  12195  oddpwdclemxy  12196  qnumdencl  12214  qnumdenbi  12219  crth  12251  reumodprminv  12280  pythagtriplem19  12309  pceu  12322  pczpre  12324  pcdiv  12329  pc11  12358  dvdsprmpweqle  12364  prmpwdvds  12382  pockthi  12385  infpnlem2  12387  elgz  12398  4sqlem12  12429  ennnfonelemim  12470  exmidunben  12472  ctinfom  12474  ctiunctlemu1st  12480  ctiunctlemu2nd  12481  ctiunctlemudc  12483  ctiunctlemfo  12485  infpn2  12502  ptex  12762  f1ocpbllem  12780  ercpbl  12800  erlecpbl  12801  grpidvalg  12842  grpidpropdg  12843  mgmlrid  12848  issgrpd  12868  sgrppropd  12869  ismnddef  12872  sgrpidmndm  12874  ismndd  12891  mndpropd  12894  mndinvmod  12899  mnd1  12900  ismhm  12906  mhmex  12907  mhmpropd  12911  issubm  12917  insubm  12930  grppropd  12955  dfgrp2  12964  isgrpid2  12977  isgrpinv  12991  grplrinv  12994  grpidinv2  12995  grpidinv  12996  dfgrp3mlem  13035  grplactcnv  13039  releqgg  13152  eqgex  13153  eqgfval  13154  eqgval  13155  isghm  13175  ghmrn  13189  resghm  13192  ghmpropd  13215  cmnpropd  13227  ablpropd  13228  imasabl  13266  isrng  13281  rngdi  13287  rngdir  13288  rngpropd  13302  dfur2g  13309  issrg  13312  srgideu  13319  srgidmlem  13325  issrgid  13328  srg1zr  13334  isring  13347  ringideu  13364  ringidmlem  13369  isringid  13372  ringid  13373  ringpropd  13385  ring1  13404  oppr0g  13424  oppr1g  13425  reldvdsrsrg  13435  dvdsrvald  13436  dvdsrd  13437  dvdsrtr  13444  unitgrp  13459  dvdsrpropdg  13490  unitpropdg  13491  rhmopp  13519  opprsubrngg  13551  issubrg  13561  subrg1  13571  subrgugrp  13580  subrgpropd  13588  aprval  13591  aprap  13595  islmod  13600  lmodlema  13601  islmodd  13602  lmodfopnelem2  13634  lmodprop2d  13657  islssm  13666  islssmg  13667  rnglidlrng  13807  isridl  13812  df2idl2rng  13816  quscrng  13840  istopg  13936  fiinbas  13986  eltg2  13990  topbas  14004  neiint  14082  neipsm  14091  opnneissb  14092  opnssneib  14093  innei  14100  restbasg  14105  iscnp4  14155  cnpnei  14156  cnconst2  14170  cnptopresti  14175  cnptoprest  14176  cnpdis  14179  lmss  14183  lmres  14185  txbas  14195  eltx  14196  neitx  14205  txcnp  14208  txcnmpt  14210  uptx  14211  txdis  14214  txdis1cn  14215  txlm  14216  txhmeo  14256  ispsmet  14260  ismet  14281  isxmet  14282  bldisj  14338  blininf  14361  blssexps  14366  blssex  14367  ssblex  14368  xmspropd  14414  mspropd  14415  neibl  14428  metequiv  14432  bdmopn  14441  metrest  14443  xmetxp  14444  xmetxpbl  14445  xmettx  14447  metcnp3  14448  tgioo  14483  tgqioo  14484  addcncntoplem  14488  mulcncflem  14527  dedekindeu  14538  dedekindicclemicc  14547  limccl  14565  ellimc3apf  14566  limcimolemlt  14570  limccoap  14584  sin0pilem2  14640  sincosq1sgn  14684  sincosq2sgn  14685  sincosq3sgn  14686  sincosq4sgn  14687  lgsval  14842  lgsdir2lem5  14870  lgsne0  14876  2sqlem8a  14906  2sqlem8  14907  2sqlem9  14908  bj-sseq  14981  bj-charfunbi  15000  bj-nalset  15084  bj-indeq  15118  bj-2inf  15127  strcoll2  15172  strcollnft  15173  strcollnfALT  15175  sscoll2  15177  subctctexmid  15188  exmidsbthrlem  15208  sbthom  15212  qdencn  15213  ltlenmkv  15256