Theorem anbi1d 620

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 619	. 2 |- (ph -> ((th /\ ps) <-> (th /\ ch)))
3		ancom 437	. 2 |- ((ps /\ th) <-> (th /\ ps))
4		ancom 437	. 2 |- ((ch /\ th) <-> (th /\ ch))
5	2, 3, 4	3bitr4g 558	1 |- (ph -> ((ps /\ th) <-> (ch /\ th)))

Syntax hints:   -> wi 3   <-> wb 144   /\ wa 221

This theorem is referenced by:  bibi2d 621  anbi1 624  anbi12d 631  bi2anan9 635  pm5.71 753  drsb1 1212  sb7f 1380  eleq1 1577  rexeq1f 1830  reueq1f 1831  rabeqf 1854  eqvinc 1929  alexeq 1931  ceqex 1932  moi 1971  sbc3ang 2027  psstr 2202  difeq1 2205  ineq1 2262  r19.28zv 2404  ifeq1 2418  ifeq2 2419  prssg 2537  eluni 2572  csbopabg 2752  axrep1 2768  axrep2 2769  axrep3 2770  zfrepclf 2773  axsep 2776  axsep2 2778  zfauscl 2779  opthgg 2865  otthg 2866  copsexg 2868  copsex4g 2870  elopab 2888  opelopab2 2896  pocl 2922  posn 2928  ordtri4 3012  dflim2 3029  uniuni 3104  rabxfr 3125  limuni3 3206  xpeq1 3281  vtoclr 3294  opelxp 3297  opbrop 3324  coeq2 3372  opelco 3378  opelco2g 3380  opelresg 3461  resopab2 3488  elxp4 3585  elxp5 3586  fun11 3667  feq2 3728  f1eq2 3768  f1eq3 3769  foeq2 3776  ssimaexg 3880  dmfco 3884  fvco 3885  isoeq5 4005  isoini 4014  f1oiso 4018  eloprabg 4067  resoprab 4069  oprabval 4083  oprabvalig 4084  oprabval2gf 4086  oprabval3 4090  oprabval6g 4093  fparlem3 4201  fparlem4 4202  tz7.44-1 4229  rdglem2 4239  oarec 4332  ertr 4414  brecop 4447  ecopoprtrn 4452  th3qlem2 4456  th3q 4458  dom2d 4545  xpsnen 4576  xpassen 4582  pw2en 4587  mapxpen 4642  xpfi 4685  unfilem3 4696  unifi 4701  preleq 4748  zfinf 4768  r1pwcl 4833  aceq1 4875  aceq0 4876  aceq6a 4887  zfac 4891  brdom7disj 4950  brdom6disj 4951  unxpdom 4994  cardcf 5061  cfeq0 5064  cfsuc 5065  cdaeng 5076  axrepnd 5100  axunndlem1 5101  axinfnd 5112  axacndlem5 5117  axacnd 5118  zfcndrep 5120  zfcndinf 5124  zfcndac 5125  ltsopq 5229  ltrpq 5239  genpass 5266  distrlem1pr 5281  distrlem5pr 5285  ltprord 5288  reclem2pr 5311  reclem3pr 5312  recexpr 5314  ltsosr 5357  mulgt0sr 5368  ltresr 5412  ltsor 5415  pre-axmulgt0 5444  ltxr 5649  lt2add 5797  le2add 5798  addgt0 5801  addgegt0 5802  addge0 5804  mulge0 5833  mulge0OLD 5834  ltrec 6029  lerec 6030  lt2msq 6031  le2msq 6048  supxr2 6250  supxrre 6251  prime 6366  peano5uzti 6375  uzindOLD 6379  qbtwnre 6418  qbtwnxr 6419  iooval 6492  iocval 6501  icoval 6502  iccval 6503  icoun 6540  snunioolem 6541  rexuz 6571  fzval 6597  sq11 6826  nn0opth2 6869  sqrlem12 6885  sqrle 6914  sqr00 6915  sqr2irrlem2 6926  cru 6939  lenegsq 7088  abs2difabs 7106  abs3lem 7110  cau3ii 7117  cau3iri 7118  sumeq1 7185  dffsum 7201  fsumsplit 7223  climfnn 7295  climunii 7301  climuni 7302  dfisum 7395  cncfval 7469  znnenlem 7713  basis2 7827  tg2 7833  tgval3 7837  tgss2 7849  neival 7927  isneip 7930  qdensere 7961  iscn 7968  cnpval 7969  iscnp 7970  blfval 8045  opni 8074  opnin 8079  neibl 8087  metcnp 8098  metcn 8100  cncfmet 8116  lmfval 8136  iscau 8147  bcthlem15 8224  isgrp2i 8293  gxoprval 8313  drngi 8408  vci 8414  isvclem 8443  ipfval 8606  nmofval 8679  isph 8737  spwval2 8915  pilem1 8938  sincosq2sgn 8972  sincosq4sgn 8974  efifolem3 8996  norm3lemt 9295  hlimi 9332  hlim2 9336  closedsub 9369  hlimuniii 9384  hlimunii 9385  occllem8 9456  projlem1 9462  projlem7 9468  projlem20 9481  shlub 9630  cmbr 9803  eigre 10041  eigorth 10044  cvbr 10490  mdbr 10502  dmdbr 10507  chrelat2 10578  mdsymlem2 10613  elo 10733  eloi 10817  islatalg 10831  vri 10981  sallnei 11016  osneisi 11018  subsp 11056  qusp 11068  cnfilca 11088  topsinind 11136  isalg 11175  algi 11181  isded 11190  dedi 11191  iscat 11208  cati 11209  cmpasso 11227  isfuna 11288  efp2 11321  trer 11409  finminlem 11418  fictb 11423  cnsubsp2 11484  compfipin0 11493  reconnlem5 11511  ivthALT 11515  1stcclb 11532  2ndc1stc 11538  2ndcctbss 11539  isfne3 11543  fnessex 11545  comppfsc 11578  fnemeet1 11589  ist1-2 11603  ist1-3 11604  t1sep 11607  nrmsep2 11616  ufileu 11658  ufinffr 11663  ufilen 11664  flimopn 11679  hausfillim 11685  cnpfillim 11686  filmapf 11688  flimff 11707  fcluscf 11724  ufcomp 11734  dirtr 11753  dirge 11754  tailf 11756  filnetlem1 11763  filnetlem2 11764  filnetlem3 11765  filnetlem4 11766  filnetlem5 11767  filnet 11768  gapmlem 11783  difin2 11791  respreima 11795  opabex3 11806  oprabopabf 11807  resoprab2 11809  acdcg 11842  add20 11858  sdclem2 11876  sdc 11877  blssp 11908  metsstop 11909  cnss 11953  lmtlm 11969  txcn 11979  txcnoprab 11981  2txcn 11982  totbndss 11993  ismtyhmeolem 12006  heiborlem25 12035  heiborlem26 12036  heiborlem28 12038  heiborlem30 12040  phtpyfval 12088  phtpyval 12089  phtpcval 12100  isphtpc 12101

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 145  df-an 223

Copyright terms: Public domain