Theorem anbi1d 752

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 751	. 2 |- (ph -> ((th /\ ps) <-> (th /\ ch)))
3		ancom 414	. 2 |- ((ps /\ th) <-> (th /\ ps))
4		ancom 414	. 2 |- ((ch /\ th) <-> (th /\ ch))
5	2, 3, 4	3bitr4g 745	1 |- (ph -> ((ps /\ th) <-> (ch /\ th)))

Syntax hints:   -> wi 3   <-> wb 219   /\ wa 337

This theorem is referenced by:  bibi2d 753  anbi1 756  anbi12d 763  bi2anan9 950  pm5.71 1061  drsb1 1819  eleq1 2204  rexeqf 2509  reueq1f 2510  rabeqf 2534  alexeq 2630  ceqex 2631  moi 2681  sbc5g 2712  rmoi 2772  psstr 2936  ineq1 3002  difin2 3064  r19.28z 3161  r19.28zv 3164  ifeq1 3183  eluni 3369  csbopabg 3577  axrep1 3597  axrep2 3598  axrep3 3599  zfrepclf 3602  axsep 3605  axsep2 3607  zfauscl 3608  opthgg 3697  otthg 3698  copsexg 3700  copsex4g 3703  elopab 3721  opelopab2 3730  pocl 3756  posn 3762  dflim2 3866  uniuni 3944  eusv2OLD 3963  eusv2 3964  reusv2lem4 3970  rabxfrd 3988  limuni3 4073  xpeq1 4149  vtoclr 4167  opbrop 4197  opelco 4259  opelco2g 4261  opelresg 4347  resopab2 4376  elxp4 4482  elxp5 4483  fun11 4581  feq2 4648  f1eq2 4693  f1eq3 4694  foeq2 4702  ssimaexg 4815  dmfco 4821  fvco 4822  respreima 4872  opabex3 4933  isoeq5 4962  isoini 4973  f1oiso 4977  f1oiso2 4978  oprabid 5002  eloprabg 5029  resoprab 5031  oprabval 5045  oprabvalig 5046  oprabval2gf 5049  oprabval3 5053  oprabval6g 5056  oprabopabf 5170  fparlem3 5206  fparlem4 5207  frxp 5210  xporderlem 5211  poxp 5212  fnwelem 5215  smoel2 5274  tz7.44-1 5300  rdglem2 5310  oarec 5407  omeu 5426  ertr 5492  brecop 5526  ecopoprtrn 5531  th3qlem2 5535  th3q 5537  dom2d 5624  xpsnen 5658  xpassen 5664  pw2en 5671  riotaeqdv 5730  xpen 5767  xpeng 5769  xpengOLDOLD 5770  mapen 5774  mapxpen 5780  unxpdom 5820  xpfir 5838  unfilem3 5862  unifi 5870  preleq 5940  zfinf 5962  r1pwcl 6034  r0weon 6146  aceq1 6183  aceq0 6184  aceq6a 6195  cdaeng 6245  cardcf 6271  cfeq0 6275  cfsuc 6276  cff1 6278  zfac 6315  brdom7disj 6380  brdom6disj 6381  unxpdomOLD 6411  cfeq0OLD 6446  cfsucOLD 6447  axrepnd 6464  axunndlem1 6465  axinfnd 6476  axacndlem5 6481  axacnd 6482  zfcndrep 6484  zfcndinf 6488  zfcndac 6489  ltsopq 6593  ltrpq 6603  genpass 6630  distrlem1pr 6645  distrlem5pr 6649  ltprord 6652  reclem2pr 6675  reclem3pr 6676  recexpr 6678  ltsosr 6721  mulgt0sr 6732  ltresr 6776  ltsor 6779  pre-axmulgt0 6806  ltxr 6854  lt2add 7165  le2add 7166  mulge0 7201  mulge0OLD 7202  ltrec 7400  lerec 7401  lt2msq 7402  le2msq 7419  supxr2 7631  supxrre 7632  prime 7750  peano5uzti 7759  uzindOLD 7763  qbtwnre 7805  qbtwnxr 7806  iooval 7879  iocval 7888  icoval 7889  iccval 7890  icoun 7928  snunioolem 7929  rexuz 7960  fzval 8000  sq11 8258  nn0opth2 8302  sqrlem12 8318  sqrle 8347  sqr00 8348  sqr2irrlem2 8359  cru 8372  lenegsq 8521  abs2difabs 8540  abs3lem 8544  cau3ii 8551  cau3iri 8552  sumeq1 8638  dffsum 8654  fsumsplit 8676  climfnn 8748  climunii 8754  climuni 8755  dfisum 8848  cncfval 8924  znnenlem 9169  divalg2 9302  gcdval 9309  1arithlem30 9424  1arithlem31 9425  isgrp 9464  isring 9508  basis2 9735  tg2 9742  tgval3 9746  tgss2 9758  neival 9858  isneip 9861  qdensere 9893  iscn 9900  cnpval 9901  iscnp 9902  blfval 9978  opni 10007  opnin 10012  neibl 10020  metcnp 10031  metcn 10033  cncfmet 10049  lmfval 10069  iscau 10080  bcthlem15 10157  grp2grpo 10190  isgrp2i 10229  gxoprval 10249  gapmlem 10330  drngi 10362  vci 10368  isvclem 10397  ipfval 10560  nmofval 10633  isph 10691  spwval2 10867  pilem1 10891  sincosq2sgn 10925  sincosq4sgn 10927  efifolem3 10949  txcn 11062  2txcn 11064  subspi 11079  hausfillim 11141  filmapf 11145  flimff 11155  flimopn 11159  dirtr 11194  dirge 11195  norm3lemt 11488  hlimi 11525  hlim2 11529  closedsub 11560  hlimuniii 11575  hlimunii 11576  occllem8 11647  projlem1 11653  projlem7 11659  projlem20 11672  shlub 11821  cmbr 11992  eigre 12230  eigorth 12233  cvbr 12685  mdbr 12697  dmdbr 12702  chrelat2 12773  mdsymlem2 12807  bnj957 13623  bnj1146 13714  dfon2lem6 14488  dfon2lem7 14489  dfon2lem8 14490  dfon2 14492  omopth 14504  xporderlemOLD 14601  poxpOLD 14602  frxpOLD 14604  poseq 14607  soseq 14608  sltval 14654  axdenselem5 14692  nocvxminlem 14697  axfelem12 14710  axfelem18 14716  axfelem22 14720  alexeqd 15002  fnoprvpop 15046  dfoprab4spop 15047  elo 15050  eloi 15112  infsdomnng 15135  surjsec2 15179  ispr1 15235  isprj1 15244  cbicplem 15247  prjmapcp2 15254  iscst2 15259  islatalg 15270  cur1vald 15286  prodeq1 15397  dffprod 15409  fprodadd 15448  vecval1b 15547  vecval3b 15548  vri 15587  sallnei 15630  osneisi 15632  qusp 15671  cnfilca 15693  exopcopn 15721  topsinind 15745  istopgrp 15749  topgrpi 15750  trhom 15761  ltrhom 15766  lvsovso 15832  isalg 15862  algi 15868  isded 15877  dedi 15878  iscat 15895  cati 15896  cmpasso 15914  dualalg 15925  isfuna 15976  tarval2 16059  tarval2g 16060  vtarsuelt 16082  efp2 16100  isplibg2 16121  trer 16185  finminlem 16191  fictb 16195  cnsubsp2 16251  compfipin0 16260  reconnlem5 16274  ivthALT 16278  1stcclb 16295  2ndc1stc 16301  2ndcctbss 16302  isfne3 16306  fnessex 16308  comppfsc 16341  fnemeet1 16352  ist1-2 16366  ist1-3 16367  t1sep 16370  nrmsep2 16379  ufileu 16397  ufinffr 16402  ufilen 16403  cnpfillim 16413  fcluscf 16436  ufcomp 16446  tailf 16457  filnetlem1 16464  filnetlem2 16465  filnetlem3 16466  filnetlem4 16467  filnetlem5 16468  filnet 16469  cover2 16497  cover2g 16498  difin2OLD 16500  respreimaOLD 16508  xpengOLD 16515  opabex3OLD 16525  fvopabf4g 16527  oprabvalg 16530  resoprab2 16534  eropreu 16557  eroprv 16558  acdcg 16574  add20 16601  sdclem2 16634  sdc 16635  fdc 16636  fdc1 16637  blssp 16668  cnss 16716  lmtlm 16732  txcnoprab 16735  cnresoprab 16739  cnoprab1 16745  cnoprab2 16746  totbndss 16761  ismtyhmeolem 16774  heiborlem25 16803  heiborlem26 16804  heiborlem28 16806  heiborlem30 16808  phtpyfval 16870  phtpyval 16871  phtpcval 16882  isphtpc 16883  pcofval 16896  pcoval 16897  pi1bval 16912  isdivrng1 16933  isriscg 16962  iscringd 16971  isfldidl2 17041  ertr2 17081  2sbc6g 17203  2sbc5g 17204  iotasbc 17207  dropab1 17248  dropab2 17249  cvrval 17661  cvrnbtwn3 17667  iscvlat2 17721  ishlat3 17750  hlrelat5 17796  3dim0 17853  issrng 17888  islvec 17900  isphil 17907  llnexatOLD 17953  llnexat 17954  islpln5 17966  islvol5 18011  pointpsub 18183  pmapjat1 18285  ltrnu 18474  cdleme02 18591

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 220  df-an 339

Copyright terms: Public domain