Theorem anbi12d 464

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 460	. 2 |- ( ph -> ( ( ps /\ th ) <-> ( ch /\ th ) ) )
3		anbi12d.2	. . 3 |- ( ph -> ( th <-> ta ) )
4	3	anbi2d 459	. 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  594  pm5.17dc  889  orbididc  937  3anbi123d  1290  xorbi2d  1358  xorbi1d  1359  drsb1  1771  mopick  2077  clelab  2265  cbvrexf  2649  cbvreu  2652  cbvrexdva2  2662  cbvrab  2684  gencbvex  2732  rspce  2784  eqvincf  2810  ceqsrexv  2815  elrabf  2838  rexab2  2850  reu2  2872  reu6  2873  rmo4  2877  reu8  2880  reuind  2889  sbcan  2951  sbcang  2952  sbcabel  2990  rmob  3001  cbvrexcsf  3063  cbvreucsf  3064  cbvrabcsf  3065  difjust  3072  injust  3076  eldif  3080  ssconb  3209  elin  3259  opeq1  3705  opeq2  3706  2ralunsn  3725  elunii  3741  csbunig  3744  eluniab  3748  cbvopab  3999  cbvopab1  4001  cbvopab2  4002  cbvopab1s  4003  cbvopab2v  4005  cbvmptf  4022  cbvmpt  4023  trel  4033  nalset  4058  elssabg  4073  mss  4148  exss  4149  opelopab2a  4187  poeq1  4221  pocl  4225  soeq1  4237  weeq1  4278  weeq2  4279  ordeq  4294  zfun  4356  snnex  4369  reusv3  4381  ontr2exmid  4440  regexmid  4450  onintexmid  4487  reg3exmid  4494  peano5  4512  limom  4527  nnregexmid  4534  vtoclr  4587  opeliunxp  4594  poinxp  4608  opbrop  4618  csbxpg  4620  opeliunxp2  4679  relop  4689  brcogw  4708  elrnmpt1  4790  elsnres  4856  dfres2  4871  inimasn  4956  xpcanm  4978  xpcan2m  4979  elxp4  5026  elxp5  5027  cnvsom  5082  sbcfung  5147  funopg  5157  fununi  5191  funcnvuni  5192  fneq1  5211  2elresin  5234  feq1  5255  sbcfng  5270  sbcfg  5271  f1eq1  5323  foeq1  5341  f1oeq1  5356  f1oeq2  5357  f1oeq3  5358  ffoss  5399  brprcneu  5414  fv3  5444  tz6.12f  5450  ssimaex  5482  fvopab3g  5494  fvopab3ig  5495  fvopab6  5517  fmptco  5586  elunirn  5667  f1imaeq  5676  foeqcnvco  5691  fliftfun  5697  fliftval  5701  isoeq1  5702  isoeq4  5705  isoini  5719  isopolem  5723  f1oiso2  5728  riotabidv  5732  cbvriota  5740  acexmid  5773  ovanraleqv  5798  cbvoprab1  5843  cbvoprab2  5844  cbvoprab12  5845  cbvmpox  5849  ov  5890  ovig  5892  ovg  5909  caovimo  5964  caoftrn  6007  opabex3d  6019  opabex3  6020  elxp6  6067  unielxp  6072  dfoprab4  6090  dfoprab4f  6091  fmpox  6098  xporderlem  6128  poxp  6129  cnvoprab  6131  f1od2  6132  opeliunxp2f  6135  rbropapd  6139  dftpos4  6160  tpostpos  6161  smoiso  6199  tfrlem3ag  6206  tfrlem3a  6207  tfr0dm  6219  tfrlemisucaccv  6222  tfrlemiex  6228  tfrlemi1  6229  tfrlemi14d  6230  tfrexlem  6231  tfr1onlem3ag  6234  tfr1onlemsucaccv  6238  tfr1onlemex  6244  tfr1onlemaccex  6245  tfr1onlemres  6246  tfrcllemsucaccv  6251  tfrcllembxssdm  6253  tfrcllemex  6257  tfrcllemaccex  6258  tfrcllemres  6259  tfrcldm  6260  frec0g  6294  frecabcl  6296  freccllem  6299  frecfcllem  6301  frecsuclem  6303  frecsuc  6304  nnacan  6408  nnmcan  6415  nnaordex  6423  ertr  6444  brecop  6519  eroveu  6520  ecopovtrn  6526  ecopovtrng  6529  th3qlem1  6531  th3qlem2  6532  th3q  6534  elpm2r  6560  mapsncnv  6589  elixp2  6596  ixpeq1  6603  elixpsn  6629  ixpsnf1o  6630  mapsnen  6705  map1  6706  xpsnen  6715  endisj  6718  xpf1o  6738  phplem3g  6750  ssfiexmid  6770  domfiexmid  6772  findcard2s  6784  isinfinf  6791  ac6sfi  6792  fiintim  6817  fisseneq  6820  f1dmvrnfibi  6832  sbthlem2  6846  isbth  6855  supeq1  6873  supeq3  6877  supeq123d  6878  supmoti  6880  eqsupti  6883  supsnti  6892  isotilem  6893  isoti  6894  supisolem  6895  supisoex  6896  cnvinfex  6905  cnvti  6906  eqinfti  6907  infvalti  6909  updjud  6967  ctssexmid  7024  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  acfun  7063  ccfunen  7079  ltsopi  7128  recexnq  7198  recmulnqg  7199  ltsonq  7206  lt2addnq  7212  lt2mulnq  7213  ltbtwnnqq  7223  prarloclemarch2  7227  enq0sym  7240  enq0ref  7241  enq0tr  7242  enq0breq  7244  addnq0mo  7255  mulnq0mo  7256  addnnnq0  7257  mulnnnq0  7258  nqnq0a  7262  nqnq0m  7263  elinp  7282  prcdnql  7292  prcunqu  7293  prltlu  7295  prdisj  7300  prarloclemlo  7302  prarloclem3  7305  prarloclem5  7308  ltdfpr  7314  genprndl  7329  genprndu  7330  genpdisj  7331  appdivnq  7371  ltpopr  7403  ltexprlemdisj  7414  ltexprlemloc  7415  ltexprlemrl  7418  ltexprlemru  7420  ltexpri  7421  recexprlemm  7432  recexprlemdisj  7438  recexprlemloc  7439  recexprlem1ssl  7441  recexprlem1ssu  7442  recexpr  7446  aptiprleml  7447  archpr  7451  cauappcvgprlemladdru  7464  cauappcvgprlemladdrl  7465  cauappcvgprlem1  7467  cauappcvgprlemlim  7469  cauappcvgpr  7470  caucvgprlemnkj  7474  caucvgprlemnbj  7475  caucvgprlemcl  7484  caucvgpr  7490  caucvgprprlemcbv  7495  caucvgprprlemval  7496  caucvgprprlemopu  7507  caucvgprpr  7520  suplocexpr  7533  addsrmo  7551  mulsrmo  7552  addsrpr  7553  mulsrpr  7554  lttrsr  7570  recexgt0sr  7581  caucvgsrlemcau  7601  caucvgsrlemgt1  7603  caucvgsrlemoffcau  7606  caucvgsrlemoffres  7608  caucvgsr  7610  suplocsrlem  7616  ltresr  7647  pitonn  7656  peano1nnnn  7660  peano2nnnn  7661  axprecex  7688  axcnre  7689  axpre-lttrn  7692  peano5nnnn  7700  axcaucvglemcau  7706  axcaucvglemres  7707  axpre-suploclemres  7709  axpre-suploc  7710  axlttrn  7833  axsuploc  7837  letri3  7845  letr  7847  le2add  8206  lt2add  8207  ltleadd  8208  lt2sub  8222  le2sub  8223  apreap  8349  apreim  8365  apti  8384  msq11  8660  dfinfre  8714  sup3exmid  8715  cju  8719  peano5nni  8723  1nn  8731  peano2nn  8732  nn2ge  8753  nominpos  8957  elz2  9122  dfuzi  9161  uzind  9162  supinfneg  9390  infsupneg  9391  xrletri3  9588  xrletr  9591  z2ge  9609  elixx1  9680  elioo2  9704  iooshf  9735  iooneg  9771  iccneg  9772  icoshft  9773  elfz1  9795  fzdifsuc  9861  fzrev  9864  1fv  9916  exbtwnzlemstep  10025  exbtwnzlemshrink  10026  exbtwnzlemex  10027  exbtwnz  10028  rebtwn2zlemstep  10030  rebtwn2zlemshrink  10031  rebtwn2z  10032  qbtwnre  10034  qbtwnxr  10035  flval  10045  flqlelt  10049  flqbi  10063  flqbi2  10064  modqid2  10124  q2submod  10158  nnesq  10411  hashunlem  10550  zfz1isolem1  10583  zfz1iso  10584  seq3coll  10585  shftlem  10588  shftfibg  10592  shftfib  10595  shftfn  10596  2shfti  10603  cjval  10617  cjth  10618  remim  10632  caucvgrelemcau  10752  caucvgre  10753  cvg1nlemcau  10756  cvg1nlemres  10757  rexanuz2  10763  recvguniq  10767  resqrexlemgt0  10792  resqrexlemoverl  10793  resqrexlemglsq  10794  resqrexlemsqa  10796  resqrexlemex  10797  rsqrmo  10799  resqrtcl  10801  rersqrtthlem  10802  absdiflt  10864  absdifle  10865  cau3lem  10886  icodiamlt  10952  maxleast  10985  negfi  10999  minmax  11001  lemininf  11005  ltmininf  11006  xrmaxlesup  11028  xrminmax  11034  xrltmininf  11039  xrlemininf  11040  iooinsup  11046  clim  11050  clim2  11052  climshftlemg  11071  addcn2  11079  climcau  11116  summodc  11152  fsum3  11156  fsum2dlemstep  11203  fisumcom2  11207  fsum00  11231  ntrivcvgap0  11318  prodeq1f  11321  prodeq2w  11325  prodeq2  11326  prodmodc  11347  sin01bnd  11464  cos01bnd  11465  divalgmod  11624  ndvdssub  11627  zsupcllemstep  11638  infssuzex  11642  gcdsupex  11646  gcdsupcl  11647  gcddvds  11652  dvdslegcd  11653  bezoutlemmain  11686  bezoutlemex  11689  bezoutlemzz  11690  bezoutlemeu  11695  bezoutlemle  11696  bezoutlemsup  11697  dfgcd3  11698  dfgcd2  11702  gcddiv  11707  lcmval  11744  lcmcllem  11748  dvdslcm  11750  lcmledvds  11751  lcmgcdlem  11758  lcmdvds  11760  coprmgcdb  11769  ncoprmgcdne1b  11770  coprmdvds1  11772  qredeu  11778  divgcdcoprm0  11782  divgcdcoprmex  11783  isprm3  11799  pw2dvdslemn  11843  pw2dvdseu  11846  oddpwdclemxy  11847  qnumdencl  11865  qnumdenbi  11870  crth  11900  ennnfonelemim  11937  exmidunben  11939  ctinfom  11941  ctiunctlemu1st  11947  ctiunctlemu2nd  11948  ctiunctlemudc  11950  ctiunctlemfo  11952  istopg  12166  fiinbas  12216  eltg2  12222  topbas  12236  neiint  12314  neipsm  12323  opnneissb  12324  opnssneib  12325  innei  12332  restbasg  12337  iscnp4  12387  cnpnei  12388  cnconst2  12402  cnptopresti  12407  cnptoprest  12408  cnpdis  12411  lmss  12415  lmres  12417  txbas  12427  eltx  12428  neitx  12437  txcnp  12440  txcnmpt  12442  uptx  12443  txdis  12446  txdis1cn  12447  txlm  12448  txhmeo  12488  ispsmet  12492  ismet  12513  isxmet  12514  bldisj  12570  blininf  12593  blssexps  12598  blssex  12599  ssblex  12600  xmspropd  12646  mspropd  12647  neibl  12660  metequiv  12664  bdmopn  12673  metrest  12675  xmetxp  12676  xmetxpbl  12677  xmettx  12679  metcnp3  12680  tgioo  12715  tgqioo  12716  addcncntoplem  12720  mulcncflem  12759  dedekindeu  12770  dedekindicclemicc  12779  limccl  12797  ellimc3apf  12798  limcimolemlt  12802  limccoap  12816  sin0pilem2  12863  sincosq1sgn  12907  sincosq2sgn  12908  sincosq3sgn  12909  sincosq4sgn  12910  bj-sseq  12999  bj-nalset  13093  bj-indeq  13127  bj-2inf  13136  subctctexmid  13196  exmidsbthrlem  13217  sbthom  13221  qdencn  13222