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  5527  f1eq3  5528  foeq2  5545  brprcneu  5620  ssimaexg  5696  dmfco  5702  fndmdif  5740  rexsupp  5759  respreima  5763  isoeq5  5929  isoini  5942  isopolem  5946  f1oiso  5950  f1oiso2  5951  riotaeqdv  5955  acexmidlemab  5995  acexmidlemcase  5996  oprabid  6033  mpoeq123  6063  mpoeq123dva  6065  eloprabga  6091  resoprab  6100  resoprab2  6101  ov  6124  ovi3  6142  ov6g  6143  ovg  6144  caoftrn  6251  opabex3d  6266  opabex3  6267  elxp7  6316  eloprabi  6342  cnvf1o  6371  xporderlem  6377  poxp  6378  smoel2  6449  frec0g  6543  freccllem  6548  frecfcllem  6550  frecsuclem  6552  frecsuc  6553  nnaordex  6674  qliftel  6762  brecop  6772  eroveu  6773  ecopovtrn  6779  ecopovtrng  6782  th3qlem2  6785  th3q  6787  ixpsnf1o  6883  dom2lem  6923  xpsnen  6980  xpassen  6989  pw2f1odclem  6995  xpf1o  7005  opabfi  7100  ctssdccl  7278  exmidapne  7446  dfplpq2  7541  dfmpq2  7542  ltsonq  7585  enq0sym  7619  enq0ref  7620  enq0tr  7621  enq0breq  7623  addnq0mo  7634  mulnq0mo  7635  addnnnq0  7636  mulnnnq0  7637  elinp  7661  prnmaxl  7675  prnminu  7676  prarloclemlo  7681  prarloc  7690  genpdflem  7694  genpassl  7711  genpassu  7712  ltexprlemm  7787  recexprlemell  7809  recexprlemelu  7810  cauappcvgprlemdisj  7838  caucvgprlemnkj  7853  caucvgprprlemnkltj  7876  caucvgprprlemnkeqj  7877  addsrmo  7930  mulsrmo  7931  addsrpr  7932  mulsrpr  7933  lttrsr  7949  mulgt0sr  7965  ltresr  8026  axpre-lttrn  8071  axpre-mulgt0  8074  recexgt0  8727  apreap  8734  apreim  8750  aprcl  8793  aptap  8797  prime  9546  rexuz  9775  ltxr  9971  ixxval  10092  fzval  10206  eqwrd  11112  pfxeq  11228  wrd2ind  11255  sqrtrval  11511  abslt  11599  absle  11600  lenegsq  11606  abs2difabs  11619  2clim  11812  climcn2  11820  addcn2  11821  mulcn2  11823  climrecvg1n  11859  sumeq1  11866  fsum2dlemstep  11945  modfsummod  11969  prodeq1f  12063  fprod2dlemstep  12133  nndivdvds  12307  divalg2  12437  gcdval  12480  bezoutlemstep  12518  bezoutlemmain  12519  bezoutlemex  12522  gcdass  12536  lcmval  12585  lcmass  12607  rpexp  12675  pythagtriplem2  12789  pythagtrip  12806  gsumfzval  13424  issgrpv  13437  issgrpn0  13438  ismhm  13494  mhmpropd  13499  issubm  13505  issubg  13710  issubg3  13729  ringpropd  14001  crngpropd  14002  opprunitd  14074  issubrg  14185  resrhm2b  14213  islmod  14255  lmodlema  14256  lmodprop2d  14312  islssm  14321  islssmg  14322  lsslss  14345  znleval  14617  psrbag  14633  istopg  14673  basis2  14722  tg2  14734  iscld  14777  neival  14817  isnei  14818  isneip  14820  iscn  14871  cnpval  14872  iscnp  14873  txbas  14932  txdis1cn  14952  ispsmet  14997  ismet  15018  isxmet  15019  ismet2  15028  blres  15108  elmopn  15120  mopni  15156  neibl  15165  metrest  15180  elcncf  15247  mulc1cncf  15263  mulcncf  15282  limccnp2lem  15350  sincosq2sgn  15501  sincosq4sgn  15503  2lgslem1a  15767  edgssv2en  15997  uhgr2edg  16004  bdsep2  16249  bdzfauscl  16253  bj-d0clsepcl  16288  sscoll2  16351