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  608  pm5.71dc  967  dfifp4dc  989  dfifp5dc  990  xorbi1d  1423  drsb1  1845  ax11ev  1874  eleq1w  2290  eleq1  2292  rexeqf  2725  reueq1f  2726  rmoeq1f  2727  rabeqf  2789  vtocl2gaf  2868  alexeq  2929  ceqex  2930  elrabi  2956  sbc5  3052  rexss  3291  ineq1  3398  difin2  3466  r19.28m  3581  elif  3614  preq12bg  3851  opeq1  3857  eluni  3891  disjiun  4078  mpteq12f  4164  axsep2  4203  zfauscl  4204  opthg  4324  copsexg  4330  euotd  4341  elopab  4346  pocl  4394  uniuni  4542  rabxfrd  4560  ontr2exmid  4617  regexmidlemm  4624  regexmidlem1  4625  reg2exmidlema  4626  preleq  4647  xpeq1  4733  elxpi  4735  vtoclr  4767  opbrop  4798  opelresg  5012  resopab2  5052  elxp4  5216  elxp5  5217  cnvpom  5271  fun11  5388  feq2  5457  f1eq2  5529  f1eq3  5530  foeq2  5547  brprcneu  5622  ssimaexg  5698  dmfco  5704  fndmdif  5742  rexsupp  5761  respreima  5765  isoeq5  5935  isoini  5948  isopolem  5952  f1oiso  5956  f1oiso2  5957  riotaeqdv  5961  acexmidlemab  6001  acexmidlemcase  6002  oprabid  6039  mpoeq123  6069  mpoeq123dva  6071  eloprabga  6097  resoprab  6106  resoprab2  6107  ov  6130  ovi3  6148  ov6g  6149  ovg  6150  caoftrn  6257  opabex3d  6272  opabex3  6273  elxp7  6322  eloprabi  6348  cnvf1o  6377  xporderlem  6383  poxp  6384  smoel2  6455  frec0g  6549  freccllem  6554  frecfcllem  6556  frecsuclem  6558  frecsuc  6559  nnaordex  6682  qliftel  6770  brecop  6780  eroveu  6781  ecopovtrn  6787  ecopovtrng  6790  th3qlem2  6793  th3q  6795  ixpsnf1o  6891  dom2lem  6931  xpsnen  6988  xpassen  6997  pw2f1odclem  7003  xpf1o  7013  opabfi  7111  ctssdccl  7289  exmidapne  7457  dfplpq2  7552  dfmpq2  7553  ltsonq  7596  enq0sym  7630  enq0ref  7631  enq0tr  7632  enq0breq  7634  addnq0mo  7645  mulnq0mo  7646  addnnnq0  7647  mulnnnq0  7648  elinp  7672  prnmaxl  7686  prnminu  7687  prarloclemlo  7692  prarloc  7701  genpdflem  7705  genpassl  7722  genpassu  7723  ltexprlemm  7798  recexprlemell  7820  recexprlemelu  7821  cauappcvgprlemdisj  7849  caucvgprlemnkj  7864  caucvgprprlemnkltj  7887  caucvgprprlemnkeqj  7888  addsrmo  7941  mulsrmo  7942  addsrpr  7943  mulsrpr  7944  lttrsr  7960  mulgt0sr  7976  ltresr  8037  axpre-lttrn  8082  axpre-mulgt0  8085  recexgt0  8738  apreap  8745  apreim  8761  aprcl  8804  aptap  8808  prime  9557  rexuz  9787  ltxr  9983  ixxval  10104  fzval  10218  eqwrd  11125  pfxeq  11244  wrd2ind  11271  sqrtrval  11527  abslt  11615  absle  11616  lenegsq  11622  abs2difabs  11635  2clim  11828  climcn2  11836  addcn2  11837  mulcn2  11839  climrecvg1n  11875  sumeq1  11882  fsum2dlemstep  11961  modfsummod  11985  prodeq1f  12079  fprod2dlemstep  12149  nndivdvds  12323  divalg2  12453  gcdval  12496  bezoutlemstep  12534  bezoutlemmain  12535  bezoutlemex  12538  gcdass  12552  lcmval  12601  lcmass  12623  rpexp  12691  pythagtriplem2  12805  pythagtrip  12822  gsumfzval  13440  issgrpv  13453  issgrpn0  13454  ismhm  13510  mhmpropd  13515  issubm  13521  issubg  13726  issubg3  13745  ringpropd  14017  crngpropd  14018  opprunitd  14090  issubrg  14201  resrhm2b  14229  islmod  14271  lmodlema  14272  lmodprop2d  14328  islssm  14337  islssmg  14338  lsslss  14361  znleval  14633  psrbag  14649  istopg  14689  basis2  14738  tg2  14750  iscld  14793  neival  14833  isnei  14834  isneip  14836  iscn  14887  cnpval  14888  iscnp  14889  txbas  14948  txdis1cn  14968  ispsmet  15013  ismet  15034  isxmet  15035  ismet2  15044  blres  15124  elmopn  15136  mopni  15172  neibl  15181  metrest  15196  elcncf  15263  mulc1cncf  15279  mulcncf  15298  limccnp2lem  15366  sincosq2sgn  15517  sincosq4sgn  15519  2lgslem1a  15783  edgssv2en  16013  uhgr2edg  16020  vtxdfifiun  16057  trlsfvalg  16127  istrl  16129  clwwlknp  16159  bdsep2  16332  bdzfauscl  16336  bj-d0clsepcl  16371  sscoll2  16434