Theorem anbi1d 628

Description: Deduction adding a right conjunct to both sides of a logical equivalence.

Hypothesis

Ref	Expression
bid.1	|- (ph -> (ps <-> ch))

Assertion

Ref	Expression
anbi1d	|- (ph -> ((ps /\ th) <-> (ch /\ th)))

Proof of Theorem anbi1d

Step	Hyp	Ref	Expression
1		bid.1	. . 3 |- (ph -> (ps <-> ch))
2	1	anbi2d 627	. 2 |- (ph -> ((th /\ ps) <-> (th /\ ch)))
3		ancom 446	. 2 |- ((ps /\ th) <-> (th /\ ps))
4		ancom 446	. 2 |- ((ch /\ th) <-> (th /\ ch))
5	2, 3, 4	3bitr4g 566	1 |- (ph -> ((ps /\ th) <-> (ch /\ th)))

Syntax hints:   -> wi 3   <-> wb 153   /\ wa 230

This theorem is referenced by:  bibi2d 629  anbi1 632  anbi12d 639  bi2anan9 643  pm5.71 760  drsb1 1217  sb7f 1383  eleq1 1581  rexeq1f 1831  reueq1f 1832  rabeqf 1855  eqvinc 1930  alexeq 1932  ceqex 1933  moi 1972  sbc3ang 2029  psstr 2201  difeq1 2204  ineq1 2261  r19.28zv 2402  ifeq1 2416  ifeq2 2417  prssg 2526  eluni 2560  csbopabg 2733  axrep1 2749  axrep2 2750  axrep3 2751  zfrepclf 2754  axsep 2757  axsep2 2759  zfauscl 2760  opthgg 2845  otthg 2846  copsexg 2848  copsex4g 2850  elopab 2867  opelopab2 2875  pocl 2900  uniuni 2937  rabxfr 2959  ordtri4 3041  dflim2 3082  limuni3 3180  xpeq1 3257  vtoclr 3268  opelxp 3271  opbrop 3295  coeq2 3339  opelco 3345  opelcog 3347  opelresg 3431  resopab2 3455  elxp4 3510  elxp5 3511  fun11 3619  feq2 3678  f1eq2 3718  f1eq3 3719  foeq2 3726  ssimaexg 3826  dmfco 3830  fvco 3831  isoeq5 3949  isoini 3958  f1oiso 3962  tz7.44-1 3986  rdglem2 3996  eloprabg 4065  resoprab 4067  oprabval 4081  oprabvalig 4082  oprabval2gf 4084  oprabval3 4088  oprabval6g 4090  2ndconst 4155  oarec 4254  ertr 4332  brecop 4367  ecopoprtrn 4372  th3qlem2 4376  th3q 4378  dom2d 4465  xpsnen 4498  xpassen 4504  pw2en 4509  mapxpen 4560  unfilem3 4613  unifi 4618  preleq 4665  axinf 4685  r1pwcl 4749  aceq1 4791  aceq0 4792  aceq6a 4803  axac 4807  brdom7disj 4866  brdom6disj 4867  unxpdom 4909  cardcf 4976  cfeq0 4979  cfsuc 4980  axrepnd 5011  axunndlem1 5012  axinfnd 5023  axacndlem5 5028  axacnd 5029  zfcndrep 5031  zfcndinf 5035  zfcndac 5036  ltsopq 5140  ltrpq 5150  genpass 5177  distrlem1pr 5192  distrlem5pr 5196  ltprord 5199  reclem2pr 5222  reclem3pr 5223  recexpr 5225  ltsosr 5268  mulgt0sr 5279  ltresr 5323  ltsor 5326  pre-axmulgt0 5355  ltxr 5560  lt2add 5708  le2add 5709  addgt0 5712  addgegt0 5713  addge0 5715  mulge0 5744  ltrec 5944  lerec 5945  lt2msq 5946  le2msq 5963  supxr2 6164  supxrre 6165  prime 6280  peano5uzti 6289  uzindOLD 6293  qbtwnre 6331  qbtwnxr 6332  iooval 6391  iocval 6400  icoval 6401  iccval 6402  icoun 6439  snunioolem 6440  rexuz 6470  fzval 6495  sq11 6718  nn0opth2 6758  sqrlem12 6774  sqrle 6803  sqr00 6804  sqr2irrlem2 6815  cru 6828  lenegsq 6975  abs2difabs 6993  abs3lem 6997  cau3ii 7004  cau3iri 7005  sumeq1 7072  dffsum 7088  fsumspl 7110  climfnn 7182  climunii 7188  climuni 7189  dfisum 7281  cncfval 7354  znnenlem 7593  basis2 7704  tg2 7710  tgval3 7714  tgss2 7726  neival 7802  isneip 7805  qdensere 7836  iscn 7843  cnpval 7844  iscnp 7845  blfval 7920  opni 7949  opnin 7954  neibl 7962  metcnp 7972  metcn 7974  cncfmet 7990  lmfval 8010  iscau 8021  bcthlem15 8098  isgrp2i 8160  vci 8251  isvclem 8280  ipfval 8436  nmofval 8509  isph 8565  spwval2 8737  pilem1 8754  sincosq2sgn 8788  sincosq4sgn 8790  efifolem3 8807  norm3lemt 9102  hlimi 9139  hlim2 9143  closedsub 9176  hlimuniii 9191  hlimunii 9192  occllem8 9263  projlem1 9269  projlem7 9275  projlem20 9288  shlub 9437  cmbr 9610  eigre 9844  eigorth 9847  cvbr 10293  mdbr 10305  dmdbr 10310  chrelat2 10381  mdsymlem2 10415  elo 10530  vri 10583  subsp 10648  qusp 10649  cnfilca 10670  isalg 10735  eloi 10741  algi 10742  isded 10751  dedi 10752  iscat 10769  cati 10770  cmpasso 10788  isfuna 10838

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 154  df-an 232

Copyright terms: Public domain