Theorem anbi2d 618

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 563	. 2 |- (ph -> ((th /\ ps) -> (th /\ ch)))
4	1	biimprd 154	. . 3 |- (ph -> (ch -> ps))
5	4	anim2d 563	. 2 |- (ph -> ((th /\ ch) -> (th /\ ps)))
6	3, 5	impbid 518	1 |- (ph -> ((th /\ ps) <-> (th /\ ch)))

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

This theorem is referenced by:  anbi1d 619  bibi2d 620  anbi12d 630  bi2anan9 634  2eu6 1457  eleq2 1538  ceqsex2 1839  eqvinc 1886  ceqsrex2v 1893  moeq3 1924  moi2 1927  moi 1928  sbc5g 1957  difeq2 2157  undif4 2329  r19.27zv 2357  prssg 2476  unieq 2514  intab 2564  opabbid 2674  opthg 2794  opthgg 2795  opelopab2 2825  pocl 2850  so 2870  ordelord 2976  dflim4 3125  xpeq2 3207  vtoclr 3217  opelxpg 3222  brinxp2 3237  opbrop 3244  coeq1 3287  opelco 3294  opelcog 3296  iss 3403  elxp4 3459  elxp5 3460  xp11 3482  fununi 3569  fneq2 3589  fneu 3598  fnun 3600  feq3 3628  fcoi1 3651  foeq3 3676  funbrfv 3756  fnopabfv 3764  ssimaexg 3775  fvco 3780  fvopab3 3783  fvopab3ig 3784  fvelrn 3818  elunirnALT 3875  isoeq2 3894  isoeq3 3895  isoini 3906  f1oiso 3910  tfrlem1 3917  tz7.44-1 3934  tz7.44-2 3935  tz7.44-3 3936  rdgeq1 3940  rdgeq2 3941  oprabbid 4001  cbvoprab3v 4006  fnoprval 4023  oprabval 4029  oprabvalig 4030  oprabval2gf 4032  oprabval3 4036  oprabval6g 4038  2ndconst 4103  ertr 4280  elqsi 4297  brecop 4312  ecopoprtrn 4317  th3qlem1 4320  th3qlem2 4321  th3q 4323  pmvalg 4337  domeng 4386  dom2d 4410  xpassen 4447  xpdom2 4448  pw2en 4452  mapxpen 4501  unfilem3 4562  fiint 4572  fiintOLD 4573  inf0 4615  scott0 4727  aceq1 4739  aceq0 4740  aceq2 4741  aceq3lem 4742  aceq3 4743  aceq5lem1 4745  aceq6b 4752  axac 4755  ac6 4765  kmlem8 4782  kmlem14 4788  brdom7disj 4814  unxpdom 4855  iscard2 4865  cfval 4918  axrepndlem1 4956  axunndlem1 4959  axregnd 4968  axinfndlem1 4969  axacndlem4 4974  axacndlem5 4975  zfcndac 4983  ltsopq 5087  prcdpq 5109  prnmax 5111  genpv 5114  genpelv 5115  genpprecl 5116  genpnnp 5120  genpnmax 5122  distrlem1pr 5139  ltprord 5146  ltexprlem3 5156  ltexprlem4 5157  ltexpri 5161  reclem2pr 5169  ltsosr 5215  mulgt0sr 5226  map2psrpr 5232  suppsr 5234  supsrlem6 5242  ltresr 5270  supre 5272  ltsor 5273  pre-axmulgt0 5302  ltxrt 5507  eqleltt 5531  lt2addt 5655  le2addt 5656  addgt0t 5659  addgegt0t 5660  addge0t 5662  lesub0t 5690  mulge0t 5691  prodgt0t 5828  prodge0t 5830  ltrect 5886  lerect 5887  lt2msqt 5888  le2msqt 5905  sup3 6054  infm3 6056  infmsup 6070  supxrre 6085  primet 6197  uzwo4OLD 6212  zbtwnre 6223  qbtwnxr 6280  seq1val 6313  ser1add2 6339  ser1add 6340  shftfval 6343  ioovalt 6367  iocvalt 6376  icovalt 6377  iccvalt 6378  icoun 6414  uzwo 6456  uzwoOLD 6457  fzvalt 6470  elfzlem 6474  sq11t 6630  nn0opth2t 6669  sqrval 6672  sqrlet 6714  crut 6739  cj11t 6830  abssubne0t 6882  abs3lemt 6907  cau3ir 6915  facwordit 6944  bcvalt 6958  clim 6977  fsumsplit 7020  csbfsum 7027  fsumcom 7028  fsumrev 7029  fsummulc1 7033  clmi1 7086  clm4at 7090  climconst3 7096  climuni 7099  climaddlem3 7116  climmullem8 7127  climmulc2 7129  iserzcmp0 7143  cvgcmp3cetlem1 7188  cvgcmp3cetlem2 7189  cvgcmp3cet 7190  geolim 7237  geolim1 7239  efseq1ex 7306  efaddlem24 7361  eftlext 7378  ef1tlub 7382  ef01tlub 7386  absef01tlub 7388  ef4pt 7400  sinbndt 7466  cosbndt 7467  acdc3 7488  acdc2 7491  acdc5 7494  acdc 7496  ruclem12 7522  infxpidmlem2 7554  infmap2lem1 7581  infmap2 7583  eltopsp 7605  tpsex 7606  istps 7607  basis2t 7614  eltg2t 7618  eltg3t 7625  tgss2t 7636  basgen2t 7638  neival 7714  isnei 7715  isneip 7717  cnpfval 7754  iscnp 7757  iscnp2 7758  cnpimaex 7762  cncnplem4 7774  ismet 7795  dfms2 7796  ismsg 7797  msflem 7800  metreslem 7819  blfval 7832  blelrn 7845  isopn 7856  metcnp 7884  metcnp2 7885  metcnpi 7887  metcnpi2 7888  metcni 7891  metcnss 7895  cncfmet 7902  tgioo 7912  lmbr 7925  lmbrf 7927  lmcvg 7929  iscau3 7935  iscau4 7937  metcn4i 7969  fsumcnlem 7986  lmcau 7993  bcthlem15 8010  isgrp 8038  isgrp2i 8072  grplactfval 8092  isring 8137  ringi 8138  vci 8163  isvclem 8192  nvcni 8325  nvcni2 8326  nvcni3 8327  va1cnlem 8341  sm1cnilem 8343  nvcnpi3 8418  nvcnpi4 8419  nmofval 8421  nmoval 8422  nmosetn0 8424  nmolb 8430  nmoubi 8431  nmo0 8447  nmlno0lem 8449  isphg 8472  htthlem3 8618  spwval2 8649  spwval 8655  spwnex 8657  sincosq3sgn 8701  efifolem3 8719  norm3lemt 9014  hlim 9051  hlim2 9055  chlim 9099  hlimcaui 9101  hlimuni 9104  ocsh 9151  occllem8 9175  projlem7 9187  projlem20 9200  pjmvalt 9233  shlubt 9349  hosmvalt 9506  hommvalt 9507  hodmvalt 9508  hfsmvalt 9509  hfmmvalt 9510  cmbrt 9522  spansncvt 9593  eigortht 9759  nmopvalt 9777  elcnopt 9778  nmopsetn0 9787  nmfnvalt 9798  nmfnsetn0 9800  elcnfnt 9804  eigvecvalt 9817  nmoplbt 9826  nmopubt 9827  cnopct 9832  nmfnlbt 9843  nmfnleubt 9844  cnfnct 9849  bravalt 9862  kbvalt 9871  nmopneg 9884  nmop0 9905  nmfn0 9906  nmlnop0ALT 9915  nmopunt 9934  nmcopexlem1 9946  nmcfnexlem1 9975  branmfnt 10033  leopmulit 10061  pjnmop 10070  cvbrt 10204  mdbrt 10216  dmdbrt 10221  atom1d 10275  chrelat2t 10292  atcvat 10308  atordt 10310  atcvat2t 10311  irredlem4 10315  mdsymlem5 10329  cayleylem2 10405  bsi 10481  iseuctopg 10488  hmeogrp 10524  fillsb 10546  ismgra 10613  isalg 10624  algi 10631  isded 10640  dedi 10641  cmpasso 10677

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