Theorem anbi1d 616

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

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

This theorem is referenced by:  bibi2d 617  anbi1 620  anbi12d 627  bi2anan9 631  pm5.71 747  drsb1 1173  sb7f 1339  eleq1 1531  rexeq1f 1781  reueq1f 1782  rabeqf 1804  eqvinc 1879  alexeq 1881  ceqex 1882  moi 1921  sbc3ang 1975  psstr 2146  difeq1 2149  ineq1 2206  r19.28zv 2346  ifeq1 2360  ifeq2 2361  prssg 2468  eluni 2501  csbopabg 2673  axrep1 2689  axrep2 2690  axrep3 2691  zfrepclf 2694  axsep 2697  axsep2 2699  zfauscl 2700  opthgg 2784  otthg 2785  copsexg 2787  copsex4g 2789  elopab 2806  opelopab2 2814  pocl 2839  uniuni 2875  rabxfr 2897  ordtri4 2979  dflim2 3020  limuni3 3118  xpeq1 3195  vtoclr 3206  opelxp 3209  opbrop 3233  coeq2 3277  opelco 3283  opelcog 3285  opelresg 3366  resopab2 3390  elxp4 3445  elxp5 3446  fun11 3554  feq2 3613  f1eq2 3652  f1eq3 3653  foeq2 3660  ssimaexg 3760  dmfco 3764  fvco 3765  isoeq5 3882  isoini 3891  f1oiso 3895  tz7.44-1 3919  rdglem2 3929  eloprabg 3998  resoprab 4000  oprabval 4014  oprabvalig 4015  oprabval2gf 4017  oprabval3 4021  oprabval6g 4023  2ndconst 4087  oarec 4186  ertr 4264  brecop 4296  ecopoprtrn 4301  th3qlem2 4305  th3q 4307  dom2d 4391  xpsnen 4421  xpassen 4427  pw2en 4432  mapxpen 4481  unfilem3 4532  unifi 4538  preleq 4583  axinf 4603  r1pwcl 4667  aceq1 4709  aceq0 4710  aceq6a 4721  axac 4725  brdom7disj 4784  brdom6disj 4785  unxpdom 4824  cardcf 4891  cfeq0 4894  cfsuc 4895  axrepnd 4926  axunndlem1 4927  axinfnd 4938  axacndlem5 4943  axacnd 4944  zfcndrep 4946  zfcndinf 4950  zfcndac 4951  ltsopq 5055  ltrpq 5065  genpass 5092  distrlem1pr 5107  distrlem5pr 5111  ltprord 5114  reclem2pr 5137  reclem3pr 5138  recexpr 5140  ltsosr 5183  mulgt0sr 5194  ltresr 5238  ltsor 5241  pre-axmulgt0 5270  ltxrt 5475  lt2addt 5625  le2addt 5626  addgt0t 5628  addgegt0t 5629  addge0t 5631  mulge0t 5660  ltrect 5840  lerect 5841  lt2msqt 5842  le2msqt 5859  supxr2 6037  supxrre 6038  primet 6150  peano5uzt 6160  uzindOLD 6164  qbtwnre 6224  qbtwnxr 6225  ioovalt 6311  iocvalt 6320  icovalt 6321  iccvalt 6322  icoun 6354  snunioolem 6355  rexuz 6384  fzvalt 6409  sq11t 6568  nn0opth2t 6606  sqrlem12 6622  sqrlet 6651  sqr00t 6652  sqr2irrlem2 6663  crut 6676  lenegsqt 6831  abs2difabst 6848  abs3lemt 6852  cau3i 6859  cau3ir 6860  sumeq1 6928  dffsum 6944  fsumsplit 6966  climfnn 7038  climunii 7043  climuni 7044  dfisum 7135  cncfval 7207  znnenlem 7451  basis2t 7565  tg2t 7571  tgval3t 7575  tgss2t 7587  neival 7667  isneip 7670  qdensere 7701  iscn 7708  cnpval 7709  iscnp 7710  blfval 7787  opni 7816  opnin 7821  neibl 7829  metcnp 7839  metcn 7841  cncfmet 7857  lmfval 7877  iscau 7888  bcthlem15 7963  isgrp2i 8026  vci 8119  isvclem 8148  ipfval 8299  nmofval 8370  isph 8425  spwval2 8595  pilem1 8609  sincosq2sgn 8641  sincosq4sgn 8643  efifolem3 8658  norm3lemt 8958  hlim 8995  hlim2 8999  closedsub 9032  hlimunii 9047  hlimuni 9048  occllem8 9119  projlem1 9125  projlem7 9131  projlem20 9144  shlubt 9292  cmbrt 9467  eigret 9701  eigortht 9704  cvbrt 10147  mdbrt 10159  dmdbrt 10164  chrelat2t 10234  mdsymlem2 10268  elo 10381  subsp 10465  qusp 10466  cnfilca 10487  isalg 10533  eloi 10539  algi 10540  isded 10549  dedi 10550  iscat 10567  cati 10568  cmpasso 10586  isfuna 10628

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