Theorem anbi12d 470

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 462	. 2 |- ( ph -> ( ( ps /\ th ) <-> ( ch /\ th ) ) )
3		anbi12d.2	. . 3 |- ( ph -> ( th <-> ta ) )
4	3	anbi2d 461	. 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-mp 5  ax-1 6  ax-2 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  600  pm5.17dc  899  orbididc  948  3anbi123d  1307  xorbi2d  1375  xorbi1d  1376  drsb1  1792  mopick  2097  clelab  2296  cbvrexfw  2688  cbvrexf  2690  cbvreu  2694  cbvrexvw  2701  cbvreuvw  2702  cbvrexdva2  2704  cbvrab  2728  gencbvex  2776  rspce  2829  eqvincf  2855  ceqsrexv  2860  elrabf  2884  rexab2  2896  reu2  2918  reu6  2919  rmo4  2923  reu8  2926  reuind  2935  sbcan  2997  sbcang  2998  sbcabel  3036  rmob  3047  cbvrexcsf  3112  cbvreucsf  3113  cbvrabcsf  3114  difjust  3122  injust  3126  eldif  3130  ssconb  3260  elin  3310  opeq1  3763  opeq2  3764  2ralunsn  3783  elunii  3799  csbunig  3802  eluniab  3806  cbvopab  4058  cbvopab1  4060  cbvopab2  4061  cbvopab1s  4062  cbvopab2v  4064  cbvmptf  4081  cbvmpt  4082  trel  4092  nalset  4117  elssabg  4132  mss  4209  exss  4210  opelopab2a  4248  poeq1  4282  pocl  4286  soeq1  4298  weeq1  4339  weeq2  4340  ordeq  4355  zfun  4417  snnex  4431  reusv3  4443  ontr2exmid  4507  regexmid  4517  onintexmid  4555  reg3exmid  4562  peano5  4580  limom  4596  nnregexmid  4603  vtoclr  4657  opeliunxp  4664  poinxp  4678  opbrop  4688  csbxpg  4690  opeliunxp2  4749  relop  4759  brcogw  4778  elrnmpt1  4860  elsnres  4926  dfres2  4941  inimasn  5026  xpcanm  5048  xpcan2m  5049  elxp4  5096  elxp5  5097  cnvsom  5152  sbcfung  5220  funopg  5230  fununi  5264  funcnvuni  5265  fneq1  5284  2elresin  5307  feq1  5328  sbcfng  5343  sbcfg  5344  f1eq1  5396  foeq1  5414  f1oeq1  5429  f1oeq2  5430  f1oeq3  5431  ffoss  5472  brprcneu  5487  fv3  5517  tz6.12f  5523  ssimaex  5555  fvopab3g  5567  fvopab3ig  5568  fvopab6  5590  fmptco  5660  elunirn  5743  f1imaeq  5752  foeqcnvco  5767  fliftfun  5773  fliftval  5777  isoeq1  5778  isoeq4  5781  isoini  5795  isopolem  5799  f1oiso2  5804  riotabidv  5809  cbvriota  5817  acexmid  5850  ovanraleqv  5875  cbvoprab1  5923  cbvoprab2  5924  cbvoprab12  5925  cbvmpox  5929  ov  5970  ovig  5972  ovg  5989  caovimo  6044  caoftrn  6084  opabex3d  6098  opabex3  6099  elxp6  6146  unielxp  6151  dfoprab4  6169  dfoprab4f  6170  fmpox  6177  xporderlem  6208  poxp  6209  cnvoprab  6211  f1od2  6212  opeliunxp2f  6215  rbropapd  6219  dftpos4  6240  tpostpos  6241  smoiso  6279  tfrlem3ag  6286  tfrlem3a  6287  tfr0dm  6299  tfrlemisucaccv  6302  tfrlemiex  6308  tfrlemi1  6309  tfrlemi14d  6310  tfrexlem  6311  tfr1onlem3ag  6314  tfr1onlemsucaccv  6318  tfr1onlemex  6324  tfr1onlemaccex  6325  tfr1onlemres  6326  tfrcllemsucaccv  6331  tfrcllembxssdm  6333  tfrcllemex  6337  tfrcllemaccex  6338  tfrcllemres  6339  tfrcldm  6340  frec0g  6374  frecabcl  6376  freccllem  6379  frecfcllem  6381  frecsuclem  6383  frecsuc  6384  nnacan  6489  nnmcan  6496  nnaordex  6504  ertr  6525  brecop  6600  eroveu  6601  ecopovtrn  6607  ecopovtrng  6610  th3qlem1  6612  th3qlem2  6613  th3q  6615  elpm2r  6641  mapsncnv  6670  elixp2  6677  ixpeq1  6684  elixpsn  6710  ixpsnf1o  6711  mapsnen  6786  map1  6787  xpsnen  6796  endisj  6799  xpf1o  6819  phplem3g  6831  ssfiexmid  6851  domfiexmid  6853  findcard2s  6865  isinfinf  6872  ac6sfi  6873  fiintim  6903  fisseneq  6906  f1dmvrnfibi  6918  sbthlem2  6932  isbth  6941  supeq1  6960  supeq3  6964  supeq123d  6965  supmoti  6967  eqsupti  6970  supsnti  6979  isotilem  6980  isoti  6981  supisolem  6982  supisoex  6983  cnvinfex  6992  cnvti  6993  eqinfti  6994  infvalti  6996  updjud  7056  ctssexmid  7123  omniwomnimkv  7140  exmidfodomrlemr  7168  exmidfodomrlemrALT  7169  acfun  7173  ccfunen  7215  cc2lem  7217  cc3  7219  ltsopi  7271  recexnq  7341  recmulnqg  7342  ltsonq  7349  lt2addnq  7355  lt2mulnq  7356  ltbtwnnqq  7366  prarloclemarch2  7370  enq0sym  7383  enq0ref  7384  enq0tr  7385  enq0breq  7387  addnq0mo  7398  mulnq0mo  7399  addnnnq0  7400  mulnnnq0  7401  nqnq0a  7405  nqnq0m  7406  elinp  7425  prcdnql  7435  prcunqu  7436  prltlu  7438  prdisj  7443  prarloclemlo  7445  prarloclem3  7448  prarloclem5  7451  ltdfpr  7457  genprndl  7472  genprndu  7473  genpdisj  7474  appdivnq  7514  ltpopr  7546  ltexprlemdisj  7557  ltexprlemloc  7558  ltexprlemrl  7561  ltexprlemru  7563  ltexpri  7564  recexprlemm  7575  recexprlemdisj  7581  recexprlemloc  7582  recexprlem1ssl  7584  recexprlem1ssu  7585  recexpr  7589  aptiprleml  7590  archpr  7594  cauappcvgprlemladdru  7607  cauappcvgprlemladdrl  7608  cauappcvgprlem1  7610  cauappcvgprlemlim  7612  cauappcvgpr  7613  caucvgprlemnkj  7617  caucvgprlemnbj  7618  caucvgprlemcl  7627  caucvgpr  7633  caucvgprprlemcbv  7638  caucvgprprlemval  7639  caucvgprprlemopu  7650  caucvgprpr  7663  suplocexpr  7676  addsrmo  7694  mulsrmo  7695  addsrpr  7696  mulsrpr  7697  lttrsr  7713  recexgt0sr  7724  caucvgsrlemcau  7744  caucvgsrlemgt1  7746  caucvgsrlemoffcau  7749  caucvgsrlemoffres  7751  caucvgsr  7753  suplocsrlem  7759  ltresr  7790  pitonn  7799  peano1nnnn  7803  peano2nnnn  7804  axprecex  7831  axcnre  7832  axpre-lttrn  7835  peano5nnnn  7843  axcaucvglemcau  7849  axcaucvglemres  7850  axpre-suploclemres  7852  axpre-suploc  7853  axlttrn  7977  axsuploc  7981  letri3  7989  letr  7991  le2add  8352  lt2add  8353  ltleadd  8354  lt2sub  8368  le2sub  8369  apreap  8495  apreim  8511  apti  8530  msq11  8807  dfinfre  8861  sup3exmid  8862  cju  8866  peano5nni  8870  1nn  8878  peano2nn  8879  nn2ge  8900  nominpos  9104  elz2  9272  dfuzi  9311  uzind  9312  supinfneg  9543  infsupneg  9544  elpqb  9597  xrletri3  9750  xrletr  9754  z2ge  9772  elixx1  9843  elioo2  9867  iooshf  9898  iooneg  9934  iccneg  9935  icoshft  9936  elfz1  9959  fzdifsuc  10026  fzrev  10029  1fv  10084  exbtwnzlemstep  10193  exbtwnzlemshrink  10194  exbtwnzlemex  10195  exbtwnz  10196  rebtwn2zlemstep  10198  rebtwn2zlemshrink  10199  rebtwn2z  10200  qbtwnre  10202  qbtwnxr  10203  flval  10217  flqlelt  10221  flqbi  10235  flqbi2  10236  modqid2  10296  q2submod  10330  nnesq  10584  hashunlem  10728  zfz1isolem1  10764  zfz1iso  10765  seq3coll  10766  shftlem  10769  shftfibg  10773  shftfib  10776  shftfn  10777  2shfti  10784  cjval  10798  cjth  10799  remim  10813  caucvgrelemcau  10933  caucvgre  10934  cvg1nlemcau  10937  cvg1nlemres  10938  rexanuz2  10944  recvguniq  10948  resqrexlemgt0  10973  resqrexlemoverl  10974  resqrexlemglsq  10975  resqrexlemsqa  10977  resqrexlemex  10978  rsqrmo  10980  resqrtcl  10982  rersqrtthlem  10983  absdiflt  11045  absdifle  11046  cau3lem  11067  icodiamlt  11133  maxleast  11166  negfi  11180  minmax  11182  lemininf  11186  ltmininf  11187  xrmaxlesup  11211  xrminmax  11217  xrltmininf  11222  xrlemininf  11223  iooinsup  11229  clim  11233  clim2  11235  climshftlemg  11254  addcn2  11262  climcau  11299  summodc  11335  fsum3  11339  fsum2dlemstep  11386  fisumcom2  11390  fsum00  11414  ntrivcvgap0  11501  prodeq1f  11504  prodeq2w  11508  prodeq2  11509  prodmodc  11530  zproddc  11531  fprodseq  11535  fprodntrivap  11536  fprod2dlemstep  11574  fprodcom2fi  11578  sin01bnd  11709  cos01bnd  11710  divalgmod  11875  ndvdssub  11878  zsupcllemstep  11889  infssuzex  11893  nninfdcex  11897  zsupssdc  11898  gcdsupex  11901  gcdsupcl  11902  gcddvds  11907  dvdslegcd  11908  bezoutlemmain  11942  bezoutlemex  11945  bezoutlemzz  11946  bezoutlemeu  11951  bezoutlemle  11952  bezoutlemsup  11953  dfgcd3  11954  dfgcd2  11958  gcddiv  11963  lcmval  12006  lcmcllem  12010  dvdslcm  12012  lcmledvds  12013  lcmgcdlem  12020  lcmdvds  12022  coprmgcdb  12031  ncoprmgcdne1b  12032  coprmdvds1  12034  qredeu  12040  divgcdcoprm0  12044  divgcdcoprmex  12045  isprm3  12061  pw2dvdslemn  12108  pw2dvdseu  12111  oddpwdclemxy  12112  qnumdencl  12130  qnumdenbi  12135  crth  12167  reumodprminv  12196  pythagtriplem19  12225  pceu  12238  pczpre  12240  pcdiv  12245  pc11  12273  dvdsprmpweqle  12279  prmpwdvds  12296  pockthi  12299  infpnlem2  12301  elgz  12312  ennnfonelemim  12368  exmidunben  12370  ctinfom  12372  ctiunctlemu1st  12378  ctiunctlemu2nd  12379  ctiunctlemudc  12381  ctiunctlemfo  12383  infpn2  12400  grpidvalg  12616  grpidpropdg  12617  mgmlrid  12622  ismnddef  12643  sgrpidmndm  12645  ismndd  12662  mndpropd  12665  mndinvmod  12667  mnd1  12668  ismhm  12674  mhmpropd  12678  issubm  12684  insubm  12692  grppropd  12713  dfgrp2  12721  isgrpid2  12732  istopg  12752  fiinbas  12802  eltg2  12808  topbas  12822  neiint  12900  neipsm  12909  opnneissb  12910  opnssneib  12911  innei  12918  restbasg  12923  iscnp4  12973  cnpnei  12974  cnconst2  12988  cnptopresti  12993  cnptoprest  12994  cnpdis  12997  lmss  13001  lmres  13003  txbas  13013  eltx  13014  neitx  13023  txcnp  13026  txcnmpt  13028  uptx  13029  txdis  13032  txdis1cn  13033  txlm  13034  txhmeo  13074  ispsmet  13078  ismet  13099  isxmet  13100  bldisj  13156  blininf  13179  blssexps  13184  blssex  13185  ssblex  13186  xmspropd  13232  mspropd  13233  neibl  13246  metequiv  13250  bdmopn  13259  metrest  13261  xmetxp  13262  xmetxpbl  13263  xmettx  13265  metcnp3  13266  tgioo  13301  tgqioo  13302  addcncntoplem  13306  mulcncflem  13345  dedekindeu  13356  dedekindicclemicc  13365  limccl  13383  ellimc3apf  13384  limcimolemlt  13388  limccoap  13402  sin0pilem2  13458  sincosq1sgn  13502  sincosq2sgn  13503  sincosq3sgn  13504  sincosq4sgn  13505  lgsval  13660  lgsdir2lem5  13688  lgsne0  13694  2sqlem8a  13713  2sqlem8  13714  2sqlem9  13715  bj-sseq  13788  bj-charfunbi  13808  bj-nalset  13892  bj-indeq  13926  bj-2inf  13935  strcoll2  13980  strcollnft  13981  strcollnfALT  13983  sscoll2  13985  subctctexmid  13996  exmidsbthrlem  14016  sbthom  14020  qdencn  14021