Theorem anbi1d 617

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 616	. 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 555	1 |- (ph -> ((ps /\ th) <-> (ch /\ th)))

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

This theorem is referenced by:  bibi2d 618  anbi1 621  anbi12d 628  bi2anan9 632  pm5.71 748  drsb1 1175  sb7f 1341  eleq1 1534  rexeq1f 1784  reueq1f 1785  rabeqf 1808  eqvinc 1883  alexeq 1885  ceqex 1886  moi 1925  sbc3ang 1979  psstr 2150  difeq1 2153  ineq1 2210  r19.28zv 2350  ifeq1 2364  ifeq2 2365  prssg 2472  eluni 2506  csbopabg 2678  axrep1 2694  axrep2 2695  axrep3 2696  zfrepclf 2699  axsep 2702  axsep2 2704  zfauscl 2705  opthgg 2789  otthg 2790  copsexg 2792  copsex4g 2794  elopab 2811  opelopab2 2819  pocl 2844  uniuni 2880  rabxfr 2902  ordtri4 2984  dflim2 3025  limuni3 3123  xpeq1 3200  vtoclr 3211  opelxp 3214  opbrop 3238  coeq2 3282  opelco 3288  opelcog 3290  opelresg 3374  resopab2 3398  elxp4 3453  elxp5 3454  fun11 3562  feq2 3621  f1eq2 3661  f1eq3 3662  foeq2 3669  ssimaexg 3769  dmfco 3773  fvco 3774  isoeq5 3891  isoini 3900  f1oiso 3904  tz7.44-1 3928  rdglem2 3938  eloprabg 4007  resoprab 4009  oprabval 4023  oprabvalig 4024  oprabval2gf 4026  oprabval3 4030  oprabval6g 4032  2ndconst 4097  oarec 4196  ertr 4274  brecop 4306  ecopoprtrn 4311  th3qlem2 4315  th3q 4317  dom2d 4404  xpsnen 4435  xpassen 4441  pw2en 4446  mapxpen 4495  unfilem3 4550  unifiOLD 4557  preleq 4603  axinf 4623  r1pwcl 4687  aceq1 4729  aceq0 4730  aceq6a 4741  axac 4745  brdom7disj 4804  brdom6disj 4805  unxpdom 4844  cardcf 4911  cfeq0 4914  cfsuc 4915  axrepnd 4946  axunndlem1 4947  axinfnd 4958  axacndlem5 4963  axacnd 4964  zfcndrep 4966  zfcndinf 4970  zfcndac 4971  ltsopq 5075  ltrpq 5085  genpass 5112  distrlem1pr 5127  distrlem5pr 5131  ltprord 5134  reclem2pr 5157  reclem3pr 5158  recexpr 5160  ltsosr 5203  mulgt0sr 5214  ltresr 5258  ltsor 5261  pre-axmulgt0 5290  ltxrt 5495  lt2addt 5643  le2addt 5644  addgt0t 5647  addgegt0t 5648  addge0t 5650  mulge0t 5679  ltrect 5884  lerect 5885  lt2msqt 5886  le2msqt 5903  supxr2 6082  supxrre 6083  primet 6195  peano5uzt 6204  uzindOLD 6208  qbtwnre 6278  qbtwnxr 6279  ioovalt 6366  iocvalt 6375  icovalt 6376  iccvalt 6377  icoun 6413  snunioolem 6414  rexuz 6444  fzvalt 6469  sq11t 6629  nn0opth2t 6668  sqrlem12 6684  sqrlet 6713  sqr00t 6714  sqr2irrlem2 6725  crut 6738  lenegsqt 6885  abs2difabst 6903  abs3lemt 6907  cau3i 6914  cau3ir 6915  sumeq1 6982  dffsum 6998  fsumsplit 7020  climfnn 7092  climunii 7098  climuni 7099  dfisum 7191  cncfval 7264  znnenlem 7501  basis2t 7615  tg2t 7621  tgval3t 7625  tgss2t 7637  neival 7717  isneip 7720  qdensere 7751  iscn 7758  cnpval 7759  iscnp 7760  blfval 7835  opni 7864  opnin 7869  neibl 7877  metcnp 7887  metcn 7889  cncfmet 7905  lmfval 7925  iscau 7936  bcthlem15 8013  isgrp2i 8076  vci 8167  isvclem 8196  ipfval 8352  nmofval 8425  isph 8481  spwval2 8653  pilem1 8671  sincosq2sgn 8705  sincosq4sgn 8707  efifolem3 8724  norm3lemt 9019  hlim 9056  hlim2 9060  closedsub 9093  hlimunii 9108  hlimuni 9109  occllem8 9180  projlem1 9186  projlem7 9192  projlem20 9205  shlubt 9354  cmbrt 9527  eigret 9761  eigortht 9764  cvbrt 10209  mdbrt 10221  dmdbrt 10226  chrelat2t 10297  mdsymlem2 10331  elo 10444  subsp 10554  qusp 10555  cnfilca 10583  cnfilcaOLD 10584  isalg 10653  eloi 10659  algi 10660  isded 10669  dedi 10670  iscat 10687  cati 10688  cmpasso 10706  isfuna 10754

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