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  610  pm5.71dc  970  dfifp4dc  992  dfifp5dc  993  xorbi1d  1426  drsb1  1847  ax11ev  1876  eleq1w  2292  eleq1  2294  rexeqf  2728  reueq1f  2729  rmoeq1f  2730  rabeqf  2793  vtocl2gaf  2872  alexeq  2933  ceqex  2934  elrabi  2960  sbc5  3056  rexss  3295  ineq1  3403  difin2  3471  r19.28m  3586  elif  3621  rabsnifsb  3741  preq12bg  3861  opeq1  3867  eluni  3901  disjiun  4088  mpteq12f  4174  axsep2  4213  zfauscl  4214  opthg  4336  copsexg  4342  euotd  4353  elopab  4358  pocl  4406  uniuni  4554  rabxfrd  4572  ontr2exmid  4629  regexmidlemm  4636  regexmidlem1  4637  reg2exmidlema  4638  preleq  4659  xpeq1  4745  elxpi  4747  vtoclr  4780  opbrop  4811  opelresg  5026  resopab2  5066  elxp4  5231  elxp5  5232  cnvpom  5286  fun11  5404  feq2  5473  f1eq2  5547  f1eq3  5548  foeq2  5565  brprcneu  5641  ssimaexg  5717  dmfco  5723  fndmdif  5761  respreima  5783  isoeq5  5956  isoini  5969  isopolem  5973  f1oiso  5977  f1oiso2  5978  riotaeqdv  5982  acexmidlemab  6022  acexmidlemcase  6023  oprabid  6060  mpoeq123  6090  mpoeq123dva  6092  eloprabga  6118  resoprab  6127  resoprab2  6128  ov  6151  ovi3  6169  ov6g  6170  ovg  6171  caoftrn  6277  opabex3d  6292  opabex3  6293  elxp7  6342  eloprabi  6370  cnvf1o  6399  xporderlem  6405  poxp  6406  rexsupp  6431  smoel2  6512  frec0g  6606  freccllem  6611  frecfcllem  6613  frecsuclem  6615  frecsuc  6616  nnaordex  6739  qliftel  6827  brecop  6837  eroveu  6838  ecopovtrn  6844  ecopovtrng  6847  th3qlem2  6850  th3q  6852  ixpsnf1o  6948  dom2lem  6988  modom  7037  xpsnen  7048  xpassen  7057  pw2f1odclem  7063  xpf1o  7073  opabfi  7175  ctssdccl  7370  exmidapne  7539  dfplpq2  7634  dfmpq2  7635  ltsonq  7678  enq0sym  7712  enq0ref  7713  enq0tr  7714  enq0breq  7716  addnq0mo  7727  mulnq0mo  7728  addnnnq0  7729  mulnnnq0  7730  elinp  7754  prnmaxl  7768  prnminu  7769  prarloclemlo  7774  prarloc  7783  genpdflem  7787  genpassl  7804  genpassu  7805  ltexprlemm  7880  recexprlemell  7902  recexprlemelu  7903  cauappcvgprlemdisj  7931  caucvgprlemnkj  7946  caucvgprprlemnkltj  7969  caucvgprprlemnkeqj  7970  addsrmo  8023  mulsrmo  8024  addsrpr  8025  mulsrpr  8026  lttrsr  8042  mulgt0sr  8058  ltresr  8119  axpre-lttrn  8164  axpre-mulgt0  8167  recexgt0  8819  apreap  8826  apreim  8842  aprcl  8885  aptap  8889  prime  9640  rexuz  9875  ltxr  10071  ixxval  10192  fzval  10307  eqwrd  11220  pfxeq  11343  wrd2ind  11370  sqrtrval  11640  abslt  11728  absle  11729  lenegsq  11735  abs2difabs  11748  2clim  11941  climcn2  11949  addcn2  11950  mulcn2  11952  climrecvg1n  11988  sumeq1  11995  fsum2dlemstep  12075  modfsummod  12099  prodeq1f  12193  fprod2dlemstep  12263  nndivdvds  12437  divalg2  12567  gcdval  12610  bezoutlemstep  12648  bezoutlemmain  12649  bezoutlemex  12652  gcdass  12666  lcmval  12715  lcmass  12737  rpexp  12805  pythagtriplem2  12919  pythagtrip  12936  gsumfzval  13554  issgrpv  13567  issgrpn0  13568  ismhm  13624  mhmpropd  13629  issubm  13635  issubg  13840  issubg3  13859  ringpropd  14132  crngpropd  14133  opprunitd  14205  issubrg  14316  resrhm2b  14344  islmod  14387  lmodlema  14388  lmodprop2d  14444  islssm  14453  islssmg  14454  lsslss  14477  znleval  14749  psrbag  14765  istopg  14810  basis2  14859  tg2  14871  iscld  14914  neival  14954  isnei  14955  isneip  14957  iscn  15008  cnpval  15009  iscnp  15010  txbas  15069  txdis1cn  15089  ispsmet  15134  ismet  15155  isxmet  15156  ismet2  15165  blres  15245  elmopn  15257  mopni  15293  neibl  15302  metrest  15317  elcncf  15384  mulc1cncf  15400  mulcncf  15419  limccnp2lem  15487  sincosq2sgn  15638  sincosq4sgn  15640  pellexlem3  15793  2lgslem1a  15907  edgssv2en  16140  uhgr2edg  16147  vtxdfifiun  16238  trlsfvalg  16324  istrl  16326  clwwlknp  16358  iseupth  16388  eupth2lem2dc  16400  bdsep2  16602  bdzfauscl  16606  bj-d0clsepcl  16641  sscoll2  16704