Theorem anbi2d 627

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 160	. . 3 |- (ph -> (ps -> ch))
3	2	anim2d 572	. 2 |- (ph -> ((th /\ ps) -> (th /\ ch)))
4	1	biimprd 161	. . 3 |- (ph -> (ch -> ps))
5	4	anim2d 572	. 2 |- (ph -> ((th /\ ch) -> (th /\ ps)))
6	3, 5	impbid 527	1 |- (ph -> ((th /\ ps) <-> (th /\ ch)))

Syntax hints:   -> wi 3   <-> wb 153   /\ wa 230

This theorem is referenced by:  anbi1d 628  bibi2d 629  anbi12d 639  bi2anan9 643  2eu6 1497  eleq2 1582  ceqsex2 1883  eqvinc 1930  ceqsrex2v 1937  moeq3 1968  moi2 1971  moi 1972  sbc5g 2001  difeq2 2205  undif4 2377  r19.27zv 2405  prssg 2526  unieq 2564  intab 2614  opabbid 2724  opthg 2844  opthgg 2845  opelopab2 2875  pocl 2900  so 2920  ordelord 3027  dflim4 3176  xpeq2 3258  vtoclr 3268  opelxpg 3273  brinxp2 3288  opbrop 3295  coeq1 3338  opelco 3345  opelcog 3347  iss 3454  elxp4 3510  elxp5 3511  xp11 3533  fununi 3620  fneq2 3640  fneu 3649  fnun 3651  feq3 3679  fcoi1 3702  foeq3 3727  funbrfv 3807  fnopabfv 3815  ssimaexg 3826  fvco 3831  fvopab3 3834  fvopab3ig 3835  fvelrn 3869  elunirnALT 3926  isoeq2 3946  isoeq3 3947  isoini 3958  f1oiso 3962  tfrlem1 3969  tz7.44-1 3986  tz7.44-2 3987  tz7.44-3 3988  rdgeq1 3992  rdgeq2 3993  oprabbid 4053  cbvoprab3v 4058  fnoprval 4075  oprabval 4081  oprabvalig 4082  oprabval2gf 4084  oprabval3 4088  oprabval6g 4090  2ndconst 4155  ertr 4332  elqsiOLD 4351  brecop 4367  ecopoprtrn 4372  th3qlem1 4375  th3qlem2 4376  th3q 4378  pmvalg 4392  domeng 4441  dom2d 4465  xpassen 4504  xpdom2 4505  pw2en 4509  mapxpen 4560  unfilem3 4613  fiint 4620  inf0 4668  scott0 4779  aceq1 4791  aceq0 4792  aceq2 4793  aceq3lem 4794  aceq3 4795  aceq5lem1 4797  aceq6b 4804  axac 4807  ac6 4817  kmlem8 4834  kmlem14 4840  brdom7disj 4866  unxpdom 4909  iscard2 4919  cfval 4971  axrepndlem1 5009  axunndlem1 5012  axregnd 5021  axinfndlem1 5022  axacndlem4 5027  axacndlem5 5028  zfcndac 5036  ltsopq 5140  prcdpq 5162  prnmax 5164  genpv 5167  genpelv 5168  genpprecl 5169  genpnnp 5173  genpnmax 5175  distrlem1pr 5192  ltprord 5199  ltexprlem3 5209  ltexprlem4 5210  ltexpri 5214  reclem2pr 5222  ltsosr 5268  mulgt0sr 5279  map2psrpr 5285  suppsr 5287  supsrlem6 5295  ltresr 5323  supre 5325  ltsor 5326  pre-axmulgt0 5355  ltxr 5560  eqlelt 5584  lt2add 5708  le2add 5709  addgt0 5712  addgegt0 5713  addge0 5715  lesub0 5743  mulge0 5744  prodgt0 5884  prodge0 5886  ltrec 5944  lerec 5945  lt2msq 5946  le2msq 5963  sup3 6134  infm3 6136  infmsup 6150  supxrre 6165  prime 6280  uzwo4OLD 6295  zbtwnre 6306  qbtwnxr 6332  iooval 6391  iocval 6400  icoval 6401  iccval 6402  icoun 6439  uzwo 6481  uzwoOLD 6482  fzval 6495  elfzlem 6499  seq1val 6571  ser1add2i 6597  ser1addi 6598  shftfval 6601  sq11 6718  nn0opth2 6758  sqrval 6761  sqrle 6803  cru 6828  cj11 6920  abssubne0 6972  abs3lem 6997  cau3iri 7005  facwordi 7034  bcval 7048  clim 7067  fsumspl 7110  csbfsum 7117  fsumcom 7118  fsumrev 7119  fsummulc1 7123  clmi1i 7176  clm4a 7180  climconst3 7186  climuni 7189  climaddlem3 7206  climmullem8 7217  climmulc2 7219  iserzcmp0 7233  cvgcmp3cetlem1 7278  cvgcmp3cetlem2 7279  cvgcmp3ce 7280  geolim 7327  geolim1 7329  efseq1ex 7396  efaddlem24 7451  eftlex 7468  ef1tlubi 7472  ef01tlubi 7476  absef01tlubi 7478  ef4p 7491  sinbnd 7557  cosbnd 7558  acdc3 7579  acdc2 7582  acdc5 7585  acdc 7587  ruclem12 7613  infxpidmlem2 7645  infmap2lem1 7671  infmap2 7673  eltopsp 7695  tpsex 7696  istps 7697  basis2 7704  eltg2 7708  eltg3 7715  tgss2 7726  basgen2 7728  neival 7802  isnei 7803  isneip 7805  cnpfval 7842  iscnp 7845  iscnp2 7846  cnpimaex 7850  cncnplem4 7862  ismet 7883  dfms2 7884  ismsg 7885  msflem 7888  metreslem 7907  blfval 7920  blelrn 7933  isopn 7944  metcnp 7972  metcnp2 7973  metcnpi 7975  metcnpi2 7976  metcni 7979  metcnss 7983  cncfmet 7990  tgioo 8000  lmbr 8013  lmbrf 8015  lmcvg 8017  iscau3 8023  iscau4 8025  metcn4i 8057  fsumcnlem 8074  lmcau 8081  bcthlem15 8098  isgrp 8126  isgrp2i 8160  grplactfval 8180  isring 8225  ringi 8226  vci 8251  isvclem 8280  nvcni 8413  nvcni2 8414  nvcni3 8415  va1cnlem 8429  sm1cnilem 8431  nvcnpi3 8506  nvcnpi4 8507  nmofval 8509  nmoval 8510  nmosetn0 8512  nmolb 8518  nmoubi 8519  nmo0 8535  nmlno0lem 8537  isphg 8560  htthlem3 8706  spwval2 8737  spwval 8743  spwnex 8745  sincosq3sgn 8789  efifolem3 8807  norm3lemt 9102  hlimi 9139  hlim2 9143  chlimi 9187  hlimcauii 9189  hlimunii 9192  ocsh 9239  occllem8 9263  projlem7 9275  projlem20 9288  pjmval 9321  shlub 9437  hosmval 9594  hommval 9595  hodmval 9596  hfsmval 9597  hfmmval 9598  cmbr 9610  spansncv 9681  eigorth 9847  nmopval 9865  elcnop 9866  nmopsetn0 9875  nmfnval 9886  nmfnsetn0 9888  elcnfn 9892  eigvecval 9905  nmoplb 9914  nmopub 9915  cnopc 9920  nmfnlb 9931  nmfnleub 9932  cnfnc 9937  braval 9950  kbval 9959  nmopnegi 9972  nmop0 9993  nmfn0 9994  nmlnop0iALT 10003  nmopun 10022  nmcopexlem1 10034  nmcfnexlem1 10063  branmfn 10121  leopmuli 10149  pjnmopi 10158  cvbr 10293  mdbr 10305  dmdbr 10310  atom1d 10364  chrelat2 10381  atcvati 10397  atord 10399  atcvat2 10400  irredlem4 10404  mdsymlem5 10418  cayleylem2 10495  vri 10583  bsi 10589  iseuctopg 10596  hmeogrp 10632  fillsb 10654  ismgra 10724  isalg 10735  algi 10742  isded 10751  dedi 10752  cmpasso 10788

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 154  df-an 232

Copyright terms: Public domain