Theorem anbi1d 462

Description: Deduction adding a right conjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)

Hypothesis

Ref	Expression
anbid.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
anbi1d	|- ( ph -> ( ( ps /\ th ) <-> ( ch /\ th ) ) )

Proof of Theorem anbi1d

Step	Hyp	Ref	Expression
1		anbid.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	a1d 22	. 2 |- ( ph -> ( th -> ( ps <-> ch ) ) )
3	2	pm5.32rd 448	1 |- ( ph -> ( ( ps /\ th ) <-> ( ch /\ th ) ) )

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:  anbi1  463  anbi12d  470  bi2anan9  601  pm5.71dc  956  xorbi1d  1376  drsb1  1792  ax11ev  1821  eleq1w  2231  eleq1  2233  rexeqf  2662  reueq1f  2663  rmoeq1f  2664  rabeqf  2720  vtocl2gaf  2797  alexeq  2856  ceqex  2857  elrabi  2883  sbc5  2978  rexss  3214  ineq1  3321  difin2  3389  r19.28m  3504  preq12bg  3760  opeq1  3765  eluni  3799  disjiun  3984  mpteq12f  4069  axsep2  4108  zfauscl  4109  opthg  4223  copsexg  4229  euotd  4239  elopab  4243  pocl  4288  uniuni  4436  rabxfrd  4454  ontr2exmid  4509  regexmidlemm  4516  regexmidlem1  4517  reg2exmidlema  4518  preleq  4539  xpeq1  4625  elxpi  4627  vtoclr  4659  opbrop  4690  opelresg  4898  resopab2  4938  elxp4  5098  elxp5  5099  cnvpom  5153  fun11  5265  feq2  5331  f1eq2  5399  f1eq3  5400  foeq2  5417  brprcneu  5489  ssimaexg  5558  dmfco  5564  fndmdif  5601  rexsupp  5620  respreima  5624  isoeq5  5784  isoini  5797  isopolem  5801  f1oiso  5805  f1oiso2  5806  riotaeqdv  5810  acexmidlemab  5847  acexmidlemcase  5848  oprabid  5885  mpoeq123  5912  mpoeq123dva  5914  eloprabga  5940  resoprab  5949  resoprab2  5950  ov  5972  ovi3  5989  ov6g  5990  ovg  5991  caoftrn  6086  opabex3d  6100  opabex3  6101  elxp7  6149  eloprabi  6175  cnvf1o  6204  xporderlem  6210  poxp  6211  smoel2  6282  frec0g  6376  freccllem  6381  frecfcllem  6383  frecsuclem  6385  frecsuc  6386  nnaordex  6507  qliftel  6593  brecop  6603  eroveu  6604  ecopovtrn  6610  ecopovtrng  6613  th3qlem2  6616  th3q  6618  ixpsnf1o  6714  dom2lem  6750  xpsnen  6799  xpassen  6808  xpf1o  6822  ctssdccl  7088  dfplpq2  7316  dfmpq2  7317  ltsonq  7360  enq0sym  7394  enq0ref  7395  enq0tr  7396  enq0breq  7398  addnq0mo  7409  mulnq0mo  7410  addnnnq0  7411  mulnnnq0  7412  elinp  7436  prnmaxl  7450  prnminu  7451  prarloclemlo  7456  prarloc  7465  genpdflem  7469  genpassl  7486  genpassu  7487  ltexprlemm  7562  recexprlemell  7584  recexprlemelu  7585  cauappcvgprlemdisj  7613  caucvgprlemnkj  7628  caucvgprprlemnkltj  7651  caucvgprprlemnkeqj  7652  addsrmo  7705  mulsrmo  7706  addsrpr  7707  mulsrpr  7708  lttrsr  7724  mulgt0sr  7740  ltresr  7801  axpre-lttrn  7846  axpre-mulgt0  7849  recexgt0  8499  apreap  8506  apreim  8522  aprcl  8565  prime  9311  rexuz  9539  ltxr  9732  ixxval  9853  fzval  9967  sqrtrval  10964  abslt  11052  absle  11053  lenegsq  11059  abs2difabs  11072  2clim  11264  climcn2  11272  addcn2  11273  mulcn2  11275  climrecvg1n  11311  sumeq1  11318  fsum2dlemstep  11397  modfsummod  11421  prodeq1f  11515  fprod2dlemstep  11585  nndivdvds  11758  divalg2  11885  gcdval  11914  bezoutlemstep  11952  bezoutlemmain  11953  bezoutlemex  11956  gcdass  11970  lcmval  12017  lcmass  12039  rpexp  12107  pythagtriplem2  12220  pythagtrip  12237  issgrpv  12645  issgrpn0  12646  ismhm  12685  mhmpropd  12689  issubm  12695  istopg  12791  basis2  12840  tg2  12854  iscld  12897  neival  12937  isnei  12938  isneip  12940  iscn  12991  cnpval  12992  iscnp  12993  txbas  13052  txdis1cn  13072  ispsmet  13117  ismet  13138  isxmet  13139  ismet2  13148  blres  13228  elmopn  13240  mopni  13276  neibl  13285  metrest  13300  elcncf  13354  mulc1cncf  13370  mulcncf  13385  limccnp2lem  13439  sincosq2sgn  13542  sincosq4sgn  13544  bdsep2  13921  bdzfauscl  13925  bj-d0clsepcl  13960  sscoll2  14023