Theorem anbi2d 616

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

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

This theorem is referenced by:  anbi1d 617  bibi2d 618  anbi12d 628  bi2anan9 632  2eu6 1454  eleq2 1535  ceqsex2 1836  eqvinc 1883  ceqsrex2v 1890  moeq3 1921  moi2 1924  moi 1925  sbc5g 1954  difeq2 2154  undif4 2325  r19.27zv 2353  prssg 2472  unieq 2510  intab 2560  opabbid 2669  opthg 2788  opthgg 2789  opelopab2 2819  pocl 2844  so 2864  ordelord 2970  dflim4 3119  xpeq2 3201  vtoclr 3211  opelxpg 3216  brinxp2 3231  opbrop 3238  coeq1 3281  opelco 3288  opelcog 3290  iss 3397  elxp4 3453  elxp5 3454  xp11 3476  fununi 3563  fneq2 3583  fneu 3592  fnun 3594  feq3 3622  fcoi1 3645  foeq3 3670  funbrfv 3750  fnopabfv 3758  ssimaexg 3769  fvco 3774  fvopab3 3777  fvopab3ig 3778  fvelrn 3812  elunirnALT 3869  isoeq2 3888  isoeq3 3889  isoini 3900  f1oiso 3904  tfrlem1 3911  tz7.44-1 3928  tz7.44-2 3929  tz7.44-3 3930  rdgeq1 3934  rdgeq2 3935  oprabbid 3995  cbvoprab3v 4000  fnoprval 4017  oprabval 4023  oprabvalig 4024  oprabval2gf 4026  oprabval3 4030  oprabval6g 4032  2ndconst 4097  ertr 4274  elqsi 4291  brecop 4306  ecopoprtrn 4311  th3qlem1 4314  th3qlem2 4315  th3q 4317  pmvalg 4331  domeng 4380  dom2d 4404  xpassen 4441  xpdom2 4442  pw2en 4446  mapxpen 4495  unfilem3 4550  fiint 4559  fiintOLD 4560  inf0 4606  scott0 4717  aceq1 4729  aceq0 4730  aceq2 4731  aceq3lem 4732  aceq3 4733  aceq5lem1 4735  aceq6b 4742  axac 4745  ac6 4755  kmlem8 4772  kmlem14 4778  brdom7disj 4804  unxpdom 4844  iscard2 4854  cfval 4906  axrepndlem1 4944  axunndlem1 4947  axregnd 4956  axinfndlem1 4957  axacndlem4 4962  axacndlem5 4963  zfcndac 4971  ltsopq 5075  prcdpq 5097  prnmax 5099  genpv 5102  genpelv 5103  genpprecl 5104  genpnnp 5108  genpnmax 5110  distrlem1pr 5127  ltprord 5134  ltexprlem3 5144  ltexprlem4 5145  ltexpri 5149  reclem2pr 5157  ltsosr 5203  mulgt0sr 5214  map2psrpr 5220  suppsr 5222  supsrlem6 5230  ltresr 5258  supre 5260  ltsor 5261  pre-axmulgt0 5290  ltxrt 5495  eqleltt 5519  lt2addt 5643  le2addt 5644  addgt0t 5647  addgegt0t 5648  addge0t 5650  lesub0t 5678  mulge0t 5679  prodgt0t 5826  prodge0t 5828  ltrect 5884  lerect 5885  lt2msqt 5886  le2msqt 5903  sup3 6052  infm3 6054  infmsup 6068  supxrre 6083  primet 6195  uzwo4OLD 6210  zbtwnre 6221  quoremOLD 6252  qbtwnxr 6279  seq1val 6312  ser1add2 6338  ser1add 6339  shftfval 6342  ioovalt 6366  iocvalt 6375  icovalt 6376  iccvalt 6377  icoun 6413  uzwo 6455  uzwoOLD 6456  fzvalt 6469  elfzlem 6473  sq11t 6629  nn0opth2t 6668  sqrval 6671  sqrlet 6713  crut 6738  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 7465  cosbndt 7466  acdc3 7487  acdc2 7490  acdc5 7493  acdc 7495  ruclem12 7521  infxpidmlem2 7553  infmap2lem1 7579  infmap2 7581  eltopsp 7604  tpsex 7605  istps 7606  basis2t 7615  eltg2t 7619  eltg3t 7626  tgss2t 7637  basgen2t 7639  neival 7717  isnei 7718  isneip 7720  cnpfval 7757  iscnp 7760  iscnp2 7761  cnpimaex 7765  cncnplem4 7777  ismet 7798  dfms2 7799  ismsg 7800  msflem 7803  metreslem 7822  blfval 7835  blelrn 7848  isopn 7859  metcnp 7887  metcnp2 7888  metcnpi 7890  metcnpi2 7891  metcni 7894  metcnss 7898  cncfmet 7905  tgioo 7915  lmbr 7928  lmbrf 7930  lmcvg 7932  iscau3 7938  iscau4 7940  metcn4i 7972  fsumcnlem 7989  lmcau 7996  bcthlem15 8013  isgrp 8041  isgrp2i 8076  grplactfval 8096  isring 8141  ringi 8142  vci 8167  isvclem 8196  nvcni 8329  nvcni2 8330  nvcni3 8331  va1cnlem 8345  sm1cnilem 8347  nvcnpi3 8422  nvcnpi4 8423  nmofval 8425  nmoval 8426  nmosetn0 8428  nmolb 8434  nmoubi 8435  nmo0 8451  nmlno0lem 8453  isphg 8476  htthlem3 8622  spwval2 8653  spwval 8659  spwnex 8661  spwpr3OLD 8662  sincosq3sgn 8706  efifolem3 8724  norm3lemt 9019  hlim 9056  hlim2 9060  chlim 9104  hlimcaui 9106  hlimuni 9109  ocsh 9156  occllem8 9180  projlem7 9192  projlem20 9205  pjmvalt 9238  shlubt 9354  hosmvalt 9511  hommvalt 9512  hodmvalt 9513  hfsmvalt 9514  hfmmvalt 9515  cmbrt 9527  spansncvt 9598  eigortht 9764  nmopvalt 9782  elcnopt 9783  nmopsetn0 9792  nmfnvalt 9803  nmfnsetn0 9805  elcnfnt 9809  eigvecvalt 9822  nmoplbt 9831  nmopubt 9832  cnopct 9837  nmfnlbt 9848  nmfnleubt 9849  cnfnct 9854  bravalt 9867  kbvalt 9876  nmopneg 9889  nmop0 9910  nmfn0 9911  nmlnop0ALT 9920  nmopunt 9939  nmcopexlem1 9951  nmcfnexlem1 9980  branmfnt 10038  leopmulit 10066  pjnmop 10075  cvbrt 10209  mdbrt 10221  dmdbrt 10226  atom1d 10280  chrelat2t 10297  atcvat 10313  atordt 10315  atcvat2t 10316  irredlem4 10320  mdsymlem5 10334  cayleylem2 10410  bsi 10495  iseuctopg 10502  hmeogrp 10538  fillsb 10560  ismgra 10642  isalg 10653  algi 10660  isded 10669  dedi 10670  cmpasso 10706

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