Theorem anbi1d 465

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 451	1 |- ( ph -> ( ( ps /\ th ) <-> ( ch /\ th ) ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  anbi1  466  anbi12d  473  bi2anan9  606  pm5.71dc  961  xorbi1d  1381  drsb1  1799  ax11ev  1828  eleq1w  2238  eleq1  2240  rexeqf  2670  reueq1f  2671  rmoeq1f  2672  rabeqf  2729  vtocl2gaf  2806  alexeq  2865  ceqex  2866  elrabi  2892  sbc5  2988  rexss  3224  ineq1  3331  difin2  3399  r19.28m  3514  preq12bg  3775  opeq1  3780  eluni  3814  disjiun  4000  mpteq12f  4085  axsep2  4124  zfauscl  4125  opthg  4240  copsexg  4246  euotd  4256  elopab  4260  pocl  4305  uniuni  4453  rabxfrd  4471  ontr2exmid  4526  regexmidlemm  4533  regexmidlem1  4534  reg2exmidlema  4535  preleq  4556  xpeq1  4642  elxpi  4644  vtoclr  4676  opbrop  4707  opelresg  4916  resopab2  4956  elxp4  5118  elxp5  5119  cnvpom  5173  fun11  5285  feq2  5351  f1eq2  5419  f1eq3  5420  foeq2  5437  brprcneu  5510  ssimaexg  5581  dmfco  5587  fndmdif  5624  rexsupp  5643  respreima  5647  isoeq5  5809  isoini  5822  isopolem  5826  f1oiso  5830  f1oiso2  5831  riotaeqdv  5835  acexmidlemab  5872  acexmidlemcase  5873  oprabid  5910  mpoeq123  5937  mpoeq123dva  5939  eloprabga  5965  resoprab  5974  resoprab2  5975  ov  5997  ovi3  6014  ov6g  6015  ovg  6016  caoftrn  6111  opabex3d  6125  opabex3  6126  elxp7  6174  eloprabi  6200  cnvf1o  6229  xporderlem  6235  poxp  6236  smoel2  6307  frec0g  6401  freccllem  6406  frecfcllem  6408  frecsuclem  6410  frecsuc  6411  nnaordex  6532  qliftel  6618  brecop  6628  eroveu  6629  ecopovtrn  6635  ecopovtrng  6638  th3qlem2  6641  th3q  6643  ixpsnf1o  6739  dom2lem  6775  xpsnen  6824  xpassen  6833  xpf1o  6847  ctssdccl  7113  exmidapne  7262  dfplpq2  7356  dfmpq2  7357  ltsonq  7400  enq0sym  7434  enq0ref  7435  enq0tr  7436  enq0breq  7438  addnq0mo  7449  mulnq0mo  7450  addnnnq0  7451  mulnnnq0  7452  elinp  7476  prnmaxl  7490  prnminu  7491  prarloclemlo  7496  prarloc  7505  genpdflem  7509  genpassl  7526  genpassu  7527  ltexprlemm  7602  recexprlemell  7624  recexprlemelu  7625  cauappcvgprlemdisj  7653  caucvgprlemnkj  7668  caucvgprprlemnkltj  7691  caucvgprprlemnkeqj  7692  addsrmo  7745  mulsrmo  7746  addsrpr  7747  mulsrpr  7748  lttrsr  7764  mulgt0sr  7780  ltresr  7841  axpre-lttrn  7886  axpre-mulgt0  7889  recexgt0  8540  apreap  8547  apreim  8563  aprcl  8606  aptap  8610  prime  9355  rexuz  9583  ltxr  9778  ixxval  9899  fzval  10013  sqrtrval  11012  abslt  11100  absle  11101  lenegsq  11107  abs2difabs  11120  2clim  11312  climcn2  11320  addcn2  11321  mulcn2  11323  climrecvg1n  11359  sumeq1  11366  fsum2dlemstep  11445  modfsummod  11469  prodeq1f  11563  fprod2dlemstep  11633  nndivdvds  11806  divalg2  11934  gcdval  11963  bezoutlemstep  12001  bezoutlemmain  12002  bezoutlemex  12005  gcdass  12019  lcmval  12066  lcmass  12088  rpexp  12156  pythagtriplem2  12269  pythagtrip  12286  issgrpv  12817  issgrpn0  12818  ismhm  12860  mhmpropd  12864  issubm  12870  issubg  13043  issubg3  13062  ringpropd  13228  crngpropd  13229  opprunitd  13290  issubrg  13353  islmod  13392  lmodlema  13393  lmodprop2d  13449  islssm  13456  lsslss  13479  istopg  13660  basis2  13709  tg2  13721  iscld  13764  neival  13804  isnei  13805  isneip  13807  iscn  13858  cnpval  13859  iscnp  13860  txbas  13919  txdis1cn  13939  ispsmet  13984  ismet  14005  isxmet  14006  ismet2  14015  blres  14095  elmopn  14107  mopni  14143  neibl  14152  metrest  14167  elcncf  14221  mulc1cncf  14237  mulcncf  14252  limccnp2lem  14306  sincosq2sgn  14409  sincosq4sgn  14411  bdsep2  14799  bdzfauscl  14803  bj-d0clsepcl  14838  sscoll2  14901