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  964  xorbi1d  1401  drsb1  1822  ax11ev  1851  eleq1w  2266  eleq1  2268  rexeqf  2699  reueq1f  2700  rmoeq1f  2701  rabeqf  2762  vtocl2gaf  2840  alexeq  2899  ceqex  2900  elrabi  2926  sbc5  3022  rexss  3260  ineq1  3367  difin2  3435  r19.28m  3550  preq12bg  3814  opeq1  3819  eluni  3853  disjiun  4040  mpteq12f  4125  axsep2  4164  zfauscl  4165  opthg  4283  copsexg  4289  euotd  4300  elopab  4305  pocl  4351  uniuni  4499  rabxfrd  4517  ontr2exmid  4574  regexmidlemm  4581  regexmidlem1  4582  reg2exmidlema  4583  preleq  4604  xpeq1  4690  elxpi  4692  vtoclr  4724  opbrop  4755  opelresg  4967  resopab2  5007  elxp4  5171  elxp5  5172  cnvpom  5226  fun11  5342  feq2  5411  f1eq2  5479  f1eq3  5480  foeq2  5497  brprcneu  5571  ssimaexg  5643  dmfco  5649  fndmdif  5687  rexsupp  5706  respreima  5710  isoeq5  5876  isoini  5889  isopolem  5893  f1oiso  5897  f1oiso2  5898  riotaeqdv  5902  acexmidlemab  5940  acexmidlemcase  5941  oprabid  5978  mpoeq123  6006  mpoeq123dva  6008  eloprabga  6034  resoprab  6043  resoprab2  6044  ov  6067  ovi3  6085  ov6g  6086  ovg  6087  caoftrn  6193  opabex3d  6208  opabex3  6209  elxp7  6258  eloprabi  6284  cnvf1o  6313  xporderlem  6319  poxp  6320  smoel2  6391  frec0g  6485  freccllem  6490  frecfcllem  6492  frecsuclem  6494  frecsuc  6495  nnaordex  6616  qliftel  6704  brecop  6714  eroveu  6715  ecopovtrn  6721  ecopovtrng  6724  th3qlem2  6727  th3q  6729  ixpsnf1o  6825  dom2lem  6865  xpsnen  6918  xpassen  6927  pw2f1odclem  6933  xpf1o  6943  opabfi  7037  ctssdccl  7215  exmidapne  7374  dfplpq2  7469  dfmpq2  7470  ltsonq  7513  enq0sym  7547  enq0ref  7548  enq0tr  7549  enq0breq  7551  addnq0mo  7562  mulnq0mo  7563  addnnnq0  7564  mulnnnq0  7565  elinp  7589  prnmaxl  7603  prnminu  7604  prarloclemlo  7609  prarloc  7618  genpdflem  7622  genpassl  7639  genpassu  7640  ltexprlemm  7715  recexprlemell  7737  recexprlemelu  7738  cauappcvgprlemdisj  7766  caucvgprlemnkj  7781  caucvgprprlemnkltj  7804  caucvgprprlemnkeqj  7805  addsrmo  7858  mulsrmo  7859  addsrpr  7860  mulsrpr  7861  lttrsr  7877  mulgt0sr  7893  ltresr  7954  axpre-lttrn  7999  axpre-mulgt0  8002  recexgt0  8655  apreap  8662  apreim  8678  aprcl  8721  aptap  8725  prime  9474  rexuz  9703  ltxr  9899  ixxval  10020  fzval  10134  eqwrd  11036  pfxeq  11150  sqrtrval  11344  abslt  11432  absle  11433  lenegsq  11439  abs2difabs  11452  2clim  11645  climcn2  11653  addcn2  11654  mulcn2  11656  climrecvg1n  11692  sumeq1  11699  fsum2dlemstep  11778  modfsummod  11802  prodeq1f  11896  fprod2dlemstep  11966  nndivdvds  12140  divalg2  12270  gcdval  12313  bezoutlemstep  12351  bezoutlemmain  12352  bezoutlemex  12355  gcdass  12369  lcmval  12418  lcmass  12440  rpexp  12508  pythagtriplem2  12622  pythagtrip  12639  gsumfzval  13256  issgrpv  13269  issgrpn0  13270  ismhm  13326  mhmpropd  13331  issubm  13337  issubg  13542  issubg3  13561  ringpropd  13833  crngpropd  13834  opprunitd  13905  issubrg  14016  resrhm2b  14044  islmod  14086  lmodlema  14087  lmodprop2d  14143  islssm  14152  islssmg  14153  lsslss  14176  znleval  14448  psrbag  14464  istopg  14504  basis2  14553  tg2  14565  iscld  14608  neival  14648  isnei  14649  isneip  14651  iscn  14702  cnpval  14703  iscnp  14704  txbas  14763  txdis1cn  14783  ispsmet  14828  ismet  14849  isxmet  14850  ismet2  14859  blres  14939  elmopn  14951  mopni  14987  neibl  14996  metrest  15011  elcncf  15078  mulc1cncf  15094  mulcncf  15113  limccnp2lem  15181  sincosq2sgn  15332  sincosq4sgn  15334  2lgslem1a  15598  bdsep2  15859  bdzfauscl  15863  bj-d0clsepcl  15898  sscoll2  15961