Theorem anbi1d 460

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 446	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  461  anbi12d  464  bi2anan9  595  pm5.71dc  945  xorbi1d  1359  drsb1  1771  ax11ev  1800  eleq1w  2198  eleq1  2200  rexeqf  2621  reueq1f  2622  rmoeq1f  2623  rabeqf  2671  vtocl2gaf  2748  alexeq  2806  ceqex  2807  elrabi  2832  sbc5  2927  rexss  3159  ineq1  3265  difin2  3333  r19.28m  3447  preq12bg  3695  opeq1  3700  eluni  3734  disjiun  3919  mpteq12f  4003  axsep2  4042  zfauscl  4043  opthg  4155  copsexg  4161  euotd  4171  elopab  4175  pocl  4220  uniuni  4367  rabxfrd  4385  ontr2exmid  4435  regexmidlemm  4442  regexmidlem1  4443  reg2exmidlema  4444  preleq  4465  xpeq1  4548  elxpi  4550  vtoclr  4582  opbrop  4613  opelresg  4821  resopab2  4861  elxp4  5021  elxp5  5022  cnvpom  5076  fun11  5185  feq2  5251  f1eq2  5319  f1eq3  5320  foeq2  5337  brprcneu  5407  ssimaexg  5476  dmfco  5482  fndmdif  5518  rexsupp  5537  respreima  5541  isoeq5  5699  isoini  5712  isopolem  5716  f1oiso  5720  f1oiso2  5721  riotaeqdv  5724  acexmidlemab  5761  acexmidlemcase  5762  oprabid  5796  mpoeq123  5823  mpoeq123dva  5825  eloprabga  5851  resoprab  5860  resoprab2  5861  ov  5883  ovi3  5900  ov6g  5901  ovg  5902  caoftrn  6000  opabex3d  6012  opabex3  6013  elxp7  6061  eloprabi  6087  cnvf1o  6115  xporderlem  6121  poxp  6122  smoel2  6193  frec0g  6287  freccllem  6292  frecfcllem  6294  frecsuclem  6296  frecsuc  6297  nnaordex  6416  qliftel  6502  brecop  6512  eroveu  6513  ecopovtrn  6519  ecopovtrng  6522  th3qlem2  6525  th3q  6527  ixpsnf1o  6623  dom2lem  6659  xpsnen  6708  xpassen  6717  xpf1o  6731  ctssdccl  6989  dfplpq2  7155  dfmpq2  7156  ltsonq  7199  enq0sym  7233  enq0ref  7234  enq0tr  7235  enq0breq  7237  addnq0mo  7248  mulnq0mo  7249  addnnnq0  7250  mulnnnq0  7251  elinp  7275  prnmaxl  7289  prnminu  7290  prarloclemlo  7295  prarloc  7304  genpdflem  7308  genpassl  7325  genpassu  7326  ltexprlemm  7401  recexprlemell  7423  recexprlemelu  7424  cauappcvgprlemdisj  7452  caucvgprlemnkj  7467  caucvgprprlemnkltj  7490  caucvgprprlemnkeqj  7491  addsrmo  7544  mulsrmo  7545  addsrpr  7546  mulsrpr  7547  lttrsr  7563  mulgt0sr  7579  ltresr  7640  axpre-lttrn  7685  axpre-mulgt0  7688  recexgt0  8335  apreap  8342  apreim  8358  aprcl  8401  prime  9143  rexuz  9368  ltxr  9555  ixxval  9672  fzval  9785  sqrtrval  10765  abslt  10853  absle  10854  lenegsq  10860  abs2difabs  10873  2clim  11063  climcn2  11071  addcn2  11072  mulcn2  11074  climrecvg1n  11110  sumeq1  11117  fsum2dlemstep  11196  modfsummod  11220  prodeq1f  11314  nndivdvds  11488  divalg2  11612  gcdval  11637  bezoutlemstep  11674  bezoutlemmain  11675  bezoutlemex  11678  gcdass  11692  lcmval  11733  lcmass  11755  rpexp  11820  istopg  12155  basis2  12204  tg2  12218  iscld  12261  neival  12301  isnei  12302  isneip  12304  iscn  12355  cnpval  12356  iscnp  12357  txbas  12416  txdis1cn  12436  ispsmet  12481  ismet  12502  isxmet  12503  ismet2  12512  blres  12592  elmopn  12604  mopni  12640  neibl  12649  metrest  12664  elcncf  12718  mulc1cncf  12734  mulcncf  12749  limccnp2lem  12803  sincosq2sgn  12897  sincosq4sgn  12899  bdsep2  13073  bdzfauscl  13077  bj-d0clsepcl  13112