Theorem anbi1d 615

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

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223

This theorem is referenced by:  bibi2d 616  anbi1 619  anbi12d 626  bi2anan9 630  pm5.71 746  drsb1 1171  sb7f 1336  eleq1 1526  rexeq1f 1776  reueq1f 1777  rabeqf 1799  eqvinc 1874  alexeq 1876  ceqex 1877  moi 1915  sbc3ang 1969  psstr 2140  difeq1 2143  ineq1 2200  r19.28zv 2340  ifeq1 2354  ifeq2 2355  prssg 2463  eluni 2496  csbopabg 2668  axrep1 2684  axrep2 2685  axrep3 2686  zfrepclf 2689  axsep 2692  axsep2 2694  zfauscl 2695  opthgg 2779  otthg 2780  copsexg 2782  copsex4g 2784  elopab 2800  opelopab2 2808  pocl 2835  uniuni 2870  rabxfr 2892  ordtri4 2974  dflim2 3015  limuni3 3113  xpeq1 3190  vtoclr 3201  opelxp 3204  opbrop 3228  coeq2 3271  opelco 3277  opelcog 3279  opelresg 3358  resopab2 3382  elxp4 3439  elxp5 3440  fun11 3548  feq2 3607  f1eq2 3646  f1eq3 3647  foeq2 3654  ssimaexg 3754  dmfco 3758  fvco 3759  isoeq5 3876  isoini 3885  f1oiso 3889  tz7.44-1 3913  rdglem2 3923  eloprabg 3992  resoprab 3994  oprabval 4008  oprabvalig 4009  oprabval2gf 4011  oprabval3 4015  oprabval6g 4017  2ndconst 4081  oarec 4180  ertr 4258  brecop 4290  ecopoprtrn 4295  th3qlem2 4299  th3q 4301  dom2d 4385  xpsnen 4415  xpassen 4421  pw2en 4426  mapxpen 4475  unfilem3 4526  unifi 4532  preleq 4575  axinf 4595  r1pwcl 4659  aceq1 4701  aceq0 4702  aceq6a 4713  axac 4717  brdom7disj 4776  brdom6disj 4777  unxpdom 4816  cardcf 4883  cfeq0 4886  cfsuc 4887  axrepnd 4918  axunndlem1 4919  axinfnd 4930  axacndlem5 4935  axacnd 4936  zfcndrep 4938  zfcndinf 4942  zfcndac 4943  ltsopq 5047  ltrpq 5057  genpass 5084  distrlem1pr 5099  distrlem5pr 5103  ltprord 5106  reclem2pr 5129  reclem3pr 5130  recexpr 5132  ltsosr 5175  mulgt0sr 5186  ltresr 5230  ltsor 5233  pre-axmulgt0 5262  ltxrt 5467  lt2addt 5617  le2addt 5618  addgt0t 5620  addgegt0t 5621  addge0t 5623  mulge0t 5652  ltrect 5832  lerect 5833  lt2msqt 5834  le2msqt 5851  supxr2 6029  supxrre 6030  primet 6142  peano5uzt 6152  uzindOLD 6156  qbtwnre 6216  qbtwnxr 6217  ioovalt 6303  iocvalt 6312  icovalt 6313  iccvalt 6314  icoun 6346  snunioolem 6347  rexuz 6376  fzvalt 6401  sq11t 6560  nn0opth2t 6598  sqrlem12 6614  sqrlet 6643  sqr00t 6644  sqr2irrlem2 6655  crut 6668  lenegsqt 6823  abs2difabst 6840  abs3lemt 6844  cau3i 6851  cau3ir 6852  sumeq1 6920  dffsum 6936  fsumsplit 6958  climfnn 7030  climunii 7035  climuni 7036  dfisum 7127  cncfval 7199  znnenlem 7443  basis2t 7557  tg2t 7563  tgval3t 7567  tgss2t 7579  neival 7658  isneip 7661  qdensere 7691  iscn 7698  cnpval 7699  iscnp 7700  blfval 7775  opni 7804  opnin 7809  neibl 7817  metcnp 7826  metcn 7828  cncfmet 7844  lmfval 7863  iscau 7874  bcthlem15 7947  isgrp2i 8011  vci 8104  isvcgOLD 8133  isvclem 8134  ipfval 8286  nmofval 8357  isph 8412  spwval2 8577  pilem1 8590  sincosq2sgn 8622  sincosq4sgn 8624  efifolem3 8639  norm3lemt 8940  hlim 8977  hlim2 8981  closedsub 9014  hlimunii 9029  hlimuni 9030  occllem8 9096  projlem1 9102  projlem7 9108  projlem20 9121  shlubt 9269  cmbrt 9444  eigret 9678  eigortht 9681  cvbrt 10119  mdbrt 10131  dmdbrt 10136  chrelat2t 10205  mdsymlem2 10239  elo 10345  subsp 10429  qusp 10430  cnfilca 10451  isalg 10497  eloi 10503  algi 10504  isded 10513  dedi 10514  iscat 10531  cati 10532  cmpasso 10550  isfuna 10592

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 147  df-an 225

Copyright terms: Public domain