Theorem anbi2d 615

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

Hypothesis

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

Assertion

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

Proof of Theorem anbi2d

Step	Hyp	Ref	Expression
1		bid.1	. . . 4 |- (ph -> (ps <-> ch))
2	1	biimpd 153	. . 3 |- (ph -> (ps -> ch))
3	2	anim2d 560	. 2 |- (ph -> ((th /\ ps) -> (th /\ ch)))
4	1	biimprd 154	. . 3 |- (ph -> (ch -> ps))
5	4	anim2d 560	. 2 |- (ph -> ((th /\ ch) -> (th /\ ps)))
6	3, 5	impbid 515	1 |- (ph -> ((th /\ ps) <-> (th /\ ch)))

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

This theorem is referenced by:  anbi1d 616  bibi2d 617  anbi12d 627  bi2anan9 631  2eu6 1452  eleq2 1532  ceqsex2 1832  eqvinc 1879  ceqsrex2v 1886  moeq3 1917  moi2 1920  moi 1921  sbc5g 1950  difeq2 2150  undif4 2321  r19.27zv 2349  prssg 2468  unieq 2505  intab 2555  opabbid 2664  opthg 2783  opthgg 2784  opelopab2 2814  pocl 2839  so 2859  ordelord 2965  dflim4 3114  xpeq2 3196  vtoclr 3206  opelxpg 3211  brinxp2 3226  opbrop 3233  coeq1 3276  opelco 3283  opelcog 3285  iss 3389  elxp4 3445  elxp5 3446  xp11 3468  fununi 3555  fneq2 3575  fneu 3584  fnun 3586  feq3 3614  fcoi1 3636  foeq3 3661  funbrfv 3741  fnopabfv 3749  ssimaexg 3760  fvco 3765  fvopab3 3768  fvopab3ig 3769  fvelrn 3803  elunirnALT 3860  isoeq2 3879  isoeq3 3880  isoini 3891  f1oiso 3895  tfrlem1 3902  tz7.44-1 3919  tz7.44-2 3920  tz7.44-3 3921  rdgeq1 3925  rdgeq2 3926  oprabbid 3986  cbvoprab3v 3991  fnoprval 4008  oprabval 4014  oprabvalig 4015  oprabval2gf 4017  oprabval3 4021  oprabval6g 4023  2ndconst 4087  ertr 4264  elqsi 4281  brecop 4296  ecopoprtrn 4301  th3qlem1 4304  th3qlem2 4305  th3q 4307  pmvalg 4321  domeng 4368  dom2d 4391  xpassen 4427  xpdom2 4428  pw2en 4432  mapxpen 4481  unfilem3 4532  fiint 4540  inf0 4586  scott0 4697  aceq1 4709  aceq0 4710  aceq2 4711  aceq3lem 4712  aceq3 4713  aceq5lem1 4715  aceq6b 4722  axac 4725  ac6 4735  kmlem8 4752  kmlem14 4758  brdom7disj 4784  unxpdom 4824  iscard2 4834  cfval 4886  axrepndlem1 4924  axunndlem1 4927  axregnd 4936  axinfndlem1 4937  axacndlem4 4942  axacndlem5 4943  zfcndac 4951  ltsopq 5055  prcdpq 5077  prnmax 5079  genpv 5082  genpelv 5083  genpprecl 5084  genpnnp 5088  genpnmax 5090  distrlem1pr 5107  ltprord 5114  ltexprlem3 5124  ltexprlem4 5125  ltexpri 5129  reclem2pr 5137  ltsosr 5183  mulgt0sr 5194  map2psrpr 5200  suppsr 5202  supsrlem6 5210  ltresr 5238  supre 5240  ltsor 5241  pre-axmulgt0 5270  ltxrt 5475  eqleltt 5500  lt2addt 5625  le2addt 5626  addgt0t 5628  addgegt0t 5629  addge0t 5631  lesub0t 5659  mulge0t 5660  prodgt0t 5790  prodge0t 5792  ltrect 5840  lerect 5841  lt2msqt 5842  le2msqt 5859  sup3 6007  infm3 6009  infmsup 6023  supxrre 6038  primet 6150  uzwo4OLD 6166  zbtwnre 6177  qbtwnxr 6225  seq1val 6257  ser1add2 6283  ser1add 6284  shftfval 6287  ioovalt 6311  iocvalt 6320  icovalt 6321  iccvalt 6322  icoun 6354  uzwo 6395  uzwoOLD 6396  fzvalt 6409  elfzlem 6413  sq11t 6568  nn0opth2t 6606  sqrval 6609  sqrlet 6651  crut 6676  cj11t 6773  abssubne0t 6828  abs3lemt 6852  cau3ir 6860  facwordit 6889  bcvalt 6903  clim 6923  fsumsplit 6966  csbfsum 6973  fsumcom 6974  fsumrev 6975  fsummulc1 6979  clmi1 7032  clm4at 7036  climconst3 7041  climuni 7044  climaddlem3 7060  climmullem8 7071  climmulc2 7073  iserzcmp0 7087  cvgcmp3cetlem1 7132  cvgcmp3cetlem2 7133  cvgcmp3cet 7134  geolim 7180  geolim1 7182  efseq1ex 7256  efaddlem24 7311  eftlext 7328  ef1tlub 7332  ef01tlub 7335  absef01tlub 7337  ef4pt 7349  sinbndt 7415  cosbndt 7416  acdc3 7437  acdc2 7440  acdc5 7443  acdc 7445  ruclem12 7472  infxpidmlem2 7504  infmap2lem1 7529  infmap2 7531  eltopsp 7554  tpsex 7555  istps 7556  basis2t 7565  eltg2t 7569  eltg3t 7576  tgss2t 7587  basgen2t 7589  neival 7667  isnei 7668  isneip 7670  cnpfval 7707  iscnp 7710  iscnp2 7711  cnpimaex 7715  cncnplem4 7727  ismet 7748  dfms2 7749  ismsg 7750  msflem 7753  metreslem 7774  blfval 7787  blelrn 7800  isopn 7811  metcnp 7839  metcnp2 7840  metcnpi 7842  metcnpi2 7843  metcni 7846  metcnss 7850  cncfmet 7857  tgioo 7867  lmbr 7880  lmbrf 7882  lmcvg 7884  iscau3 7890  iscau4 7892  metcn4i 7922  fsumcnlem 7939  lmcau 7946  bcthlem15 7963  isgrp 7991  isgrp2i 8026  grplactfval 8047  isring 8093  ringi 8094  vci 8119  isvclem 8148  nvcni 8279  va1cnlem 8292  sm1cnilem 8294  nvcnpi4 8368  nmofval 8370  nmoval 8371  nmosetn0 8373  nmolb 8379  nmoubi 8380  nmo0 8396  nmlno0lem 8398  isphg 8420  htthlem3 8565  spwval2 8595  spwval 8600  spwnex 8602  sincosq3sgn 8642  efifolem3 8658  norm3lemt 8958  hlim 8995  hlim2 8999  chlim 9043  hlimcaui 9045  hlimuni 9048  ocsh 9095  occllem8 9119  projlem7 9131  projlem20 9144  pjmvalt 9176  shlubt 9292  hosmvalt 9451  hommvalt 9452  hodmvalt 9453  hfsmvalt 9454  hfmmvalt 9455  cmbrt 9467  spansncvt 9538  eigortht 9704  nmopvalt 9722  elcnopt 9723  nmopsetn0 9732  nmfnvalt 9743  nmfnsetn0 9745  elcnfnt 9749  eigvecvalt 9762  nmoplbt 9771  nmopubt 9772  cnopct 9776  nmfnlbt 9787  nmfnleubt 9788  cnfnct 9793  bravalt 9806  kbvalt 9815  nmopneg 9828  nmop0 9849  nmfn0 9850  nmlnop0ALT 9858  nmopunt 9877  nmcopexlem1 9889  nmcfnexlem1 9918  branmfnt 9976  leopmulit 10004  pjnmop 10013  cvbrt 10147  mdbrt 10159  dmdbrt 10164  atom1d 10217  chrelat2t 10234  atcvat 10250  atordt 10252  atcvat2t 10253  irredlem4 10257  mdsymlem5 10271  cayleylem2 10344  bsi 10418  iseuctopg 10425  hmeogrp 10461  fillsb 10471  ismgra 10522  isalg 10533  algi 10540  isded 10549  dedi 10550  cmpasso 10586

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