Theorem anbi12d 457

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 453	. 2 |- ( ph -> ( ( ps /\ th ) <-> ( ch /\ th ) ) )
3		anbi12d.2	. . 3 |- ( ph -> ( th <-> ta ) )
4	3	anbi2d 452	. 2 |- ( ph -> ( ( ch /\ th ) <-> ( ch /\ ta ) ) )
5	2, 4	bitrd 186	1 |- ( ph -> ( ( ps /\ th ) <-> ( ch /\ ta ) ) )

Syntax hints:   -> wi 4   /\ wa 102   <-> wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  pm4.38  570  pm5.17dc  846  orbididc  897  3anbi123d  1246  xorbi2d  1314  xorbi1d  1315  drsb1  1724  mopick  2023  clelab  2209  cbvrexf  2581  cbvreu  2584  cbvrexdva2  2591  cbvrab  2613  gencbvex  2659  rspce  2710  eqvincf  2733  ceqsrexv  2738  elrabf  2760  rexab2  2772  reu2  2794  reu6  2795  rmo4  2799  reu8  2802  reuind  2809  sbcan  2870  sbcang  2871  sbcabel  2909  rmob  2920  cbvrexcsf  2980  cbvreucsf  2981  cbvrabcsf  2982  difjust  2989  injust  2993  eldif  2997  ssconb  3122  elin  3172  opeq1  3605  opeq2  3606  2ralunsn  3625  elunii  3641  csbunig  3644  eluniab  3648  cbvopab  3884  cbvopab1  3886  cbvopab2  3887  cbvopab1s  3888  cbvopab2v  3890  cbvmpt  3907  trel  3917  nalset  3943  elssabg  3958  mss  4026  exss  4027  opelopab2a  4065  poeq1  4099  pocl  4103  soeq1  4115  weeq1  4156  weeq2  4157  ordeq  4172  zfun  4234  snnex  4244  reusv3  4255  ontr2exmid  4313  regexmid  4323  onintexmid  4360  reg3exmid  4367  peano5  4385  limom  4400  nnregexmid  4406  vtoclr  4453  opeliunxp  4460  poinxp  4474  opbrop  4484  csbxpg  4486  opeliunxp2  4543  relop  4553  brcogw  4572  elrnmpt1  4653  elsnres  4715  dfres2  4728  inimasn  4812  xpcanm  4833  xpcan2m  4834  elxp4  4881  elxp5  4882  cnvsom  4937  sbcfung  5001  funopg  5010  fununi  5044  funcnvuni  5045  fneq1  5064  2elresin  5087  feq1  5107  sbcfng  5121  sbcfg  5122  f1eq1  5168  foeq1  5186  f1oeq1  5201  f1oeq2  5202  f1oeq3  5203  ffoss  5242  brprcneu  5255  fv3  5285  tz6.12f  5290  ssimaex  5322  fvopab3g  5334  fvopab3ig  5335  fvopab6  5353  fmptco  5421  elunirn  5500  f1imaeq  5509  foeqcnvco  5524  fliftfun  5530  fliftval  5534  isoeq1  5535  isoeq4  5538  isoini  5552  isopolem  5556  f1oiso2  5561  riotabidv  5565  cbvriota  5573  acexmid  5606  cbvoprab1  5671  cbvoprab2  5672  cbvoprab12  5673  cbvmpt2x  5677  ov  5715  ovig  5717  ovg  5734  caovimo  5789  caoftrn  5831  opabex3d  5843  opabex3  5844  elxp6  5891  unielxp  5895  dfoprab4  5913  dfoprab4f  5914  fmpt2x  5921  xporderlem  5947  poxp  5948  cnvoprab  5950  f1od2  5951  sprmpt2  5955  isprmpt2  5956  dftpos4  5976  tpostpos  5977  smoiso  6015  tfrlem3ag  6022  tfrlem3a  6023  tfr0dm  6035  tfrlemisucaccv  6038  tfrlemiex  6044  tfrlemi1  6045  tfrlemi14d  6046  tfrexlem  6047  tfr1onlem3ag  6050  tfr1onlemsucaccv  6054  tfr1onlemex  6060  tfr1onlemaccex  6061  tfr1onlemres  6062  tfrcllemsucaccv  6067  tfrcllembxssdm  6069  tfrcllemex  6073  tfrcllemaccex  6074  tfrcllemres  6075  tfrcldm  6076  frec0g  6110  frecabcl  6112  freccllem  6115  frecfcllem  6117  frecsuclem  6119  frecsuc  6120  nnacan  6217  nnmcan  6224  nnaordex  6232  ertr  6253  brecop  6328  eroveu  6329  ecopovtrn  6335  ecopovtrng  6338  th3qlem1  6340  th3qlem2  6341  th3q  6343  elpm2r  6369  mapsncnv  6398  mapsnen  6474  map1  6475  xpsnen  6483  endisj  6486  xpf1o  6506  phplem3g  6518  ssfiexmid  6538  domfiexmid  6540  findcard2s  6552  isinfinf  6559  ac6sfi  6560  fisseneq  6586  f1dmvrnfibi  6597  sbthlem2  6604  isbth  6613  supeq1  6618  supeq3  6622  supeq123d  6623  supmoti  6625  eqsupti  6628  supsnti  6637  isotilem  6638  isoti  6639  supisolem  6640  supisoex  6641  cnvinfex  6650  cnvti  6651  eqinfti  6652  infvalti  6654  updjud  6710  exmidfodomrlemr  6765  exmidfodomrlemrALT  6766  ltsopi  6816  recexnq  6886  recmulnqg  6887  ltsonq  6894  lt2addnq  6900  lt2mulnq  6901  ltbtwnnqq  6911  prarloclemarch2  6915  enq0sym  6928  enq0ref  6929  enq0tr  6930  enq0breq  6932  addnq0mo  6943  mulnq0mo  6944  addnnnq0  6945  mulnnnq0  6946  nqnq0a  6950  nqnq0m  6951  elinp  6970  prcdnql  6980  prcunqu  6981  prltlu  6983  prdisj  6988  prarloclemlo  6990  prarloclem3  6993  prarloclem5  6996  ltdfpr  7002  genprndl  7017  genprndu  7018  genpdisj  7019  appdivnq  7059  ltpopr  7091  ltexprlemdisj  7102  ltexprlemloc  7103  ltexprlemrl  7106  ltexprlemru  7108  ltexpri  7109  recexprlemm  7120  recexprlemdisj  7126  recexprlemloc  7127  recexprlem1ssl  7129  recexprlem1ssu  7130  recexpr  7134  aptiprleml  7135  archpr  7139  cauappcvgprlemladdru  7152  cauappcvgprlemladdrl  7153  cauappcvgprlem1  7155  cauappcvgprlemlim  7157  cauappcvgpr  7158  caucvgprlemnkj  7162  caucvgprlemnbj  7163  caucvgprlemcl  7172  caucvgpr  7178  caucvgprprlemcbv  7183  caucvgprprlemval  7184  caucvgprprlemopu  7195  caucvgprpr  7208  addsrmo  7226  mulsrmo  7227  addsrpr  7228  mulsrpr  7229  lttrsr  7245  recexgt0sr  7256  caucvgsrlemcau  7275  caucvgsrlemgt1  7277  caucvgsrlemoffcau  7280  caucvgsrlemoffres  7282  caucvgsr  7284  ltresr  7313  pitonn  7322  peano1nnnn  7326  peano2nnnn  7327  axprecex  7352  axcnre  7353  axpre-lttrn  7356  peano5nnnn  7364  axcaucvglemcau  7370  axcaucvglemres  7371  axlttrn  7492  letri3  7503  letr  7505  le2add  7859  lt2add  7860  ltleadd  7861  lt2sub  7875  le2sub  7876  apreap  7998  apreim  8014  apti  8033  msq11  8291  dfinfre  8345  cju  8349  peano5nni  8353  1nn  8361  peano2nn  8362  nn2ge  8382  nominpos  8579  elz2  8744  dfuzi  8782  uzind  8783  supinfneg  9008  infsupneg  9009  xrletri3  9195  xrletr  9198  z2ge  9213  elixx1  9240  elioo2  9264  iooshf  9295  iooneg  9330  iccneg  9331  icoshft  9332  elfz1  9354  fzdifsuc  9418  fzrev  9421  1fv  9471  exbtwnzlemstep  9580  exbtwnzlemshrink  9581  exbtwnzlemex  9582  exbtwnz  9583  rebtwn2zlemstep  9585  rebtwn2zlemshrink  9586  rebtwn2z  9587  qbtwnre  9589  qbtwnxr  9590  flval  9600  flqlelt  9604  flqbi  9618  flqbi2  9619  modqid2  9679  q2submod  9713  nnesq  9962  hashunlem  10101  zfz1isolem1  10134  zfz1iso  10135  iseqcoll  10136  shftlem  10139  shftfibg  10143  shftfib  10146  shftfn  10147  2shfti  10154  cjval  10167  cjth  10168  remim  10182  caucvgrelemcau  10301  caucvgre  10302  cvg1nlemcau  10305  cvg1nlemres  10306  rexanuz2  10312  recvguniq  10316  resqrexlemgt0  10341  resqrexlemoverl  10342  resqrexlemglsq  10343  resqrexlemsqa  10345  resqrexlemex  10346  rsqrmo  10348  resqrtcl  10350  rersqrtthlem  10351  absdiflt  10413  absdifle  10414  cau3lem  10435  icodiamlt  10501  maxleast  10534  negfi  10545  minmax  10547  lemininf  10550  ltmininf  10551  clim  10555  clim2  10557  climshftlemg  10576  addcn2  10584  climcau  10619  isummo  10655  fisum  10658  divalgmod  10794  ndvdssub  10797  zsupcllemstep  10808  infssuzex  10812  gcdsupex  10816  gcdsupcl  10817  gcddvds  10822  dvdslegcd  10823  bezoutlemmain  10854  bezoutlemex  10857  bezoutlemzz  10858  bezoutlemeu  10863  bezoutlemle  10864  bezoutlemsup  10865  dfgcd3  10866  dfgcd2  10870  gcddiv  10875  lcmval  10912  lcmcllem  10916  dvdslcm  10918  lcmledvds  10919  lcmgcdlem  10926  lcmdvds  10928  coprmgcdb  10937  ncoprmgcdne1b  10938  coprmdvds1  10940  qredeu  10946  divgcdcoprm0  10950  divgcdcoprmex  10951  isprm3  10967  pw2dvdslemn  11010  pw2dvdseu  11013  oddpwdclemxy  11014  qnumdencl  11032  qnumdenbi  11037  crth  11067  bj-sseq  11122  bj-nalset  11216  bj-indeq  11254  bj-2inf  11263  exmidsbthrlem  11342  qdencn  11345