MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  anbi2d Structured version   Unicode version

Theorem anbi2d 703
Description: Deduction adding a left conjunct to both sides of a logical equivalence. (Contributed by NM, 11-May-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)
Hypothesis
Ref Expression
bid.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
anbi2d  |-  ( ph  ->  ( ( th  /\  ps )  <->  ( th  /\  ch ) ) )

Proof of Theorem anbi2d
StepHypRef Expression
1 bid.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21a1d 25 . 2  |-  ( ph  ->  ( th  ->  ( ps 
<->  ch ) ) )
32pm5.32d 639 1  |-  ( ph  ->  ( ( th  /\  ps )  <->  ( th  /\  ch ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  anbi2  707  anbi12d  710  bi2anan9  871  2eu6OLD  2368  eleq2dALT  2512  eleq2OLD  2516  ceqsex2  3131  ceqsex6v  3135  vtocl2gaf  3158  vtocl4ga  3163  ceqsrex2v  3219  moeq3  3260  mob2  3263  eqreu  3275  reu2eqd  3280  nelrdva  3293  undif4  3866  r19.27z  3910  r19.27zv  3911  ssunsn2  4171  preq12bg  4191  prel12g  4192  opeq2  4200  ralunsn  4219  intab  4299  disjxun  4432  opabbid  4496  opthg  4709  pocl  4794  isso2i  4819  ordelord  4887  ordtri4  4902  xpeq2  5001  rabxp  5023  vtoclr  5031  opeliunxp  5038  posn  5055  opbrop  5066  elrnmpt1  5238  dfres2  5313  brcodir  5373  poltletr  5389  xp11  5429  fununi  5641  fneq2  5657  fnun  5674  feq3  5702  foeq3  5780  funbrfv  5893  ssimaexg  5921  fvopab3g  5934  fvopab3ig  5935  fvelrn  6006  fvcofneq  6021  fmptco  6046  elunirn  6145  f12dfv  6161  f13dfv  6162  isoeq2  6198  isoeq3  6199  isoini  6216  isopolem  6223  f1oiso  6229  f1oiso2  6230  riotabidv  6241  oprabv  6327  oprabbid  6332  cbvoprab3  6355  mpt2mptx  6375  mpt2fun  6386  elrnmpt2res  6398  ov  6404  ov3  6421  ov6g  6422  ovg  6423  caoftrn  6557  dfwe2  6599  dflim4  6665  tfisi  6675  elxp4  6726  elxp5  6727  f1o2ndf1  6890  frxp  6892  xporderlem  6893  fnwelem  6897  brtpos2  6960  dftpos4  6973  onfununi  7011  recseq  7042  omopth  7306  brecop  7403  eroveu  7405  erovlem  7406  erov  7407  ecopovtrn  7413  elpmg  7433  ixpsnval  7471  ixpsnf1o  7508  domeng  7529  dom2lem  7554  xpcomco  7606  xpassen  7610  xpdom2  7611  omxpenlem  7617  xpf1o  7678  unxpdom  7726  isinf  7732  findcard2  7759  findcard2d  7761  fiint  7796  supeq2  7907  wemapso2lem  7978  inf0  8038  cantnfp1lem3  8099  cantnfp1  8100  scott0  8304  isinffi  8373  isacn  8425  aceq1  8498  aceq0  8499  aceq2  8500  dfac3  8502  dfac5lem1  8504  dfac2  8511  dfac12lem2  8524  kmlem8  8537  kmlem14  8543  infmap2  8598  cfval  8627  cflim3  8642  sornom  8657  infpssrlem4  8686  isf32lem9  8741  domtriomlem  8822  axdc2lem  8828  zfac  8840  ac6num  8859  axrepndlem1  8967  axunndlem1  8970  axregnd  8981  axregndOLD  8982  axinfndlem1  8983  axacndlem4  8988  axacndlem5  8989  zfcndac  8997  fpwwe2lem5  9012  pwfseqlem4a  9039  pwfseqlem4  9040  alephgch  9052  wunex2  9116  tskord  9158  nqereu  9307  ordpipq  9320  prcdnq  9371  prnmax  9373  genpnnp  9383  distrlem5pr  9405  ltprord  9408  ltexprlem3  9416  ltexprlem4  9417  ltexpri  9421  prlem936  9425  reclem2pr  9426  addsrmo  9450  mulsrmo  9451  addsrpr  9452  mulsrpr  9453  ltsosr  9471  mulgt0sr  9482  ltresr  9517  axpre-lttrn  9543  axpre-mulgt0  9545  eqlelt  9672  lesub0  10072  wloglei  10088  mulle0b  10416  sup3  10503  infm3  10505  prime  10946  fzind  10964  uzwo  11150  uzwoOLD  11151  zbtwnre  11186  xltnegi  11421  xmulneg1  11467  ixxval  11543  fzval  11680  elfzm11  11755  elfzo  11807  seqof2  12141  nn0opth2  12328  facwordi  12343  hashnn0n0nn  12434  brfi1uzind  12508  wrdeqswrdlsw  12650  2swrd1eqwrdeq  12655  wrd2ind  12679  cshwcsh2id  12772  2swrd2eqwrdeq  12867  shftfval  12879  shftfib  12881  shftfn  12882  2shfti  12889  abs1m  13144  cau3lem  13163  caubnd2  13166  clim  13293  rlim  13294  clim2  13303  climi  13309  o1lo1  13336  rlimcn2  13389  climcn2  13391  addcn2  13392  subcn2  13393  mulcn2  13394  o1of2  13411  isercoll  13466  caurcvg2  13476  sumeq2w  13490  sumeq2ii  13491  summo  13515  fsum  13518  sinbnd  13789  cosbnd  13790  divalgb  13936  ndvdssub  13939  smupp1  14004  smueqlem  14014  gcdval  14020  gcdcllem2  14024  gcdneg  14038  gcdass  14057  algcvgblem  14080  prmind2  14102  qredeq  14121  euclemma  14123  qnumval  14144  qdenval  14145  eulerthlem2  14186  pceu  14244  pczpre  14245  pcdiv  14250  prmpwdvds  14296  prmreclem5  14312  vdwapun  14366  ramub2  14406  rami  14407  ramcl  14421  ismred2  14874  isacs  14922  iscatd2  14952  catpropd  14978  oppccatid  14988  isinv  15028  isssc  15063  funcres2b  15137  funcpropd  15140  fucinv  15213  yoniso  15425  prslem  15431  drsdir  15435  drsdirfi  15438  posi  15450  isposd  15456  pltval  15461  plttr  15471  isipodrs  15662  ipodrsima  15666  dirge  15738  gsumpropd  15770  gsumress  15774  mnd1OLD  15833  mrcmndind  15868  mgmnsgrpex  15920  qusgrp2  16059  resscntz  16240  psgnunilem3  16392  psgneu  16402  psgnvali  16404  psgnvalii  16405  isslw  16499  subgslw  16507  iscmnd  16681  gsumval3eu  16778  gsumval3OLD  16779  gsumval3lem2  16781  telgsumfzs  16889  dmdprd  16900  subgdmdprd  16952  dprd2d2  16964  pgpfac1  17002  pgpfaclem2  17004  pgpfaclem3  17005  pgpfac  17006  ablfaclem1  17007  qusring2  17140  dvdsrval  17165  crngunit  17182  dfrhm2  17237  isdrngd  17292  abvpropd  17362  islmod  17387  lssacs  17484  lsspropd  17534  islmhm  17544  lbspropd  17616  ixpsnbasval  17726  fiidomfld  17828  ltbval  18007  opsrval  18010  mpfind  18076  coe1fzgsumd  18215  pf1ind  18262  evl1gsumd  18264  psgndiflemA  18507  pjfval2  18610  frlmup1  18702  scmatf1  18903  mdetralt  18980  mdetralt2  18981  mdetunilem1  18984  mdetunilem2  18985  mdetunilem9  18992  gsummatr01  19031  eltopspOLD  19289  istpsOLD  19291  basis2  19322  eltg2  19329  isclo  19458  isnei  19474  isneip  19476  neiptopnei  19503  restbas  19529  restcld  19543  neitr  19551  iscnp  19608  iscnp3  19615  tgcn  19623  cnpimaex  19627  lmbrf  19631  cncnp  19651  cnprest2  19661  isreg  19703  regsep  19705  isnrm  19706  ist1-2  19718  nrmsep3  19726  isnrm2  19729  hauscmplem  19776  dfcon2  19790  is1stc  19812  1stcclb  19815  1stcfb  19816  is2ndc  19817  2ndc1stc  19822  1stcrest  19824  2ndcsep  19830  1stccnp  19833  islly  19839  llyeq  19841  llyi  19845  hausllycmp  19865  lly1stc  19867  islocfin  19888  txbas  19938  ptpjpre1  19942  elpt  19943  txcnpi  19979  ptpjopn  19983  ptcldmpt  19985  ptclsg  19986  txcnp  19991  ptcnp  19993  hausdiag  20016  tx1stc  20021  xkoinjcn  20058  imasnopn  20061  imasncld  20062  imasncls  20063  fbfinnfr  20212  snfil  20235  uffix2  20295  elfm  20318  elfm2  20319  fmco  20332  hauspwpwf1  20358  flfnei  20362  isflf  20364  lmflf  20376  fclscf  20396  isfcf  20405  alexsublem  20414  cnextcn  20437  cnextfres  20438  eltsms  20501  tsmsresOLD  20515  tsmsres  20516  tsmsf1o  20517  ustuqtop4  20617  ispsmet  20678  ismet  20696  isxmet  20697  ismet2  20706  imasdsf1olem  20746  blres  20804  met2ndc  20896  metcnp3  20913  nrmmetd  20965  pi1grplem  21419  lmmbr2  21568  lmmbrf  21571  iscau2  21586  iscau4  21588  caucfil  21592  lmclim  21611  cfilucfil3OLD  21627  cfilucfil3  21628  bcthlem1  21633  bcth  21638  ishl2  21680  pmltpclem1  21730  elovolm  21756  ovolgelb  21761  ovolicc  21804  mbfaddlem  21937  i1fres  21982  mbfi1fseqlem4  21995  itg2l  22006  itg2leub  22011  itg2seq  22019  isibl  22042  iblitg  22045  dfitg  22046  itgeq2  22054  itgvallem  22061  iblcnlem1  22064  iblrelem  22067  iblpos  22069  ellimc3  22153  limciun  22168  limcun  22169  dvmptfsum  22246  dveflem  22250  lhop1lem  22284  dvfsumlem2  22298  dvfsumlem4  22300  mdegleb  22334  elply2  22463  plypf1  22479  coeval  22490  plydivlem4  22561  sincosq3sgn  22762  vmasum  23360  lgsqrlem1  23485  lgsquadlem1  23498  2sqlem8  23516  2sqlem9  23517  2sqlem11  23519  dchrisumlema  23542  dchrisumlem2  23544  pntibndlem3  23646  pntibnd  23647  pntleme  23662  pntlemp  23664  axtgsegcon  23730  axtg5seg  23731  axtgpasch  23733  iscgrg  23773  legov  23841  ltgov  23852  ishlg  23855  mirreu3  23904  israg  23943  islnopp  23982  ishpg  23997  iscgra  24038  brcgr  24072  brbtwn2  24077  colinearalg  24082  ax5seg  24110  axcontlem5  24140  axcontlem10  24145  usgraedg4  24256  cusgrafilem2  24349  cusgrafi  24351  uvtx01vtx  24361  usgrnloop  24434  spthonepeq  24458  usgra2adedgwlkonALT  24485  usgra2wlkspthlem1  24488  usgrcyclnl2  24510  4cycl4v4e  24535  4cycl4dv4e  24537  wwlk  24550  wlklniswwlkn2  24569  clwlkisclwwlklem0  24657  clwlkisclwwlk  24658  eleclclwwlkn  24702  usghashecclwwlk  24704  el2wlkonot  24738  el2spthonot  24739  el2spthonot0  24740  usg2spthonot  24757  usg2spthonot0  24758  usg2spthonot1  24759  isrusgra  24796  isrusgusrg  24801  isrgrac  24803  isrusgrac  24804  rusgranumwlkl1  24816  iseupa  24834  eupath2lem3  24848  1vwmgra  24872  3vfriswmgra  24874  3cyclfrgrarn1  24881  4cycl2vnunb  24886  vdn1frgrav2  24894  vdgn1frgrav2  24895  frgrancvvdeqlemB  24907  usg2spot2nb  24934  usgreg2spot  24936  2spotmdisj  24937  usgreghash2spot  24938  extwwlkfab  24959  numclwwlk2lem1  24971  numclwwlk5  24981  isgrpo  25067  isgrp2d  25106  isgrpda  25168  ismndo  25214  drngoi  25278  vci  25310  isvclem  25339  nmoofval  25546  nmooval  25547  nmosetn0  25549  nmoolb  25555  nmoubi  25556  nmoo0  25575  nmlno0lem  25577  isphg  25601  norm3lemt  25938  chlimi  26021  ocsh  26070  cmbr  26371  chscllem2  26425  spansncv  26440  eigorth  26626  nmopval  26644  nmopsetn0  26653  nmfnval  26664  nmfnsetn0  26666  nmoplb  26695  nmfnlb  26712  nmopnegi  26753  nmop0  26774  nmfn0  26775  nmlnop0iALT  26783  nmopun  26802  nmcexi  26814  branmfn  26893  leopmuli  26921  pjnmopi  26936  cvbr  27070  mdbr  27082  dmdbr  27087  atom1d  27141  chrelat2  27158  atcvati  27174  atord  27176  atcvat2  27177  chirredlem4  27181  mdsymlem5  27195  disjunsn  27322  opeldifid  27325  fcoinvbr  27330  fimarab  27352  fmptcof2  27371  ofpreima  27376  funcnv4mpt  27381  mpt2mptxf  27387  2ndpreima  27394  f1od2  27416  fpwrelmapffslem  27424  xeqlelt  27456  ishashinf  27475  ressprs  27513  isomnd  27561  archiabllem2a  27608  archiabl  27612  isslmd  27615  gsumle  27640  gsumvsca1  27643  gsumvsca2  27644  orngmul  27663  ismntop  27874  esumcvg  27962  sitgval  28144  eulerpartlemmf  28184  eulerpartlemgvv  28185  eulerpartlemn  28190  eulerpart  28191  brafs  28422  lgamgulmlem2  28442  erdszelem3  28507  erdsze  28516  pconcn  28539  cnpcon  28545  txpcon  28547  conpcon  28550  cvmscbv  28573  iscvm  28574  cvmsi  28580  cvmsval  28581  mclsval  28793  mclsppslem  28813  relexp0  28922  relexpsucr  28923  relexpsucl  28925  relexpadd  28931  relexpindlem  28932  prodfdiv  29002  ntrivcvgn0  29004  ntrivcvgmullem  29007  prodeq1f  29012  prodeq2w  29016  prodeq2ii  29017  prodmo  29040  zprod  29041  fprod  29045  fprodntriv  29046  elima4  29181  dfrdg2  29200  dfrdg3  29201  elpred  29229  trpredrec  29293  poseq  29305  soseq  29306  sltval  29379  nocvxminlem  29422  nofulllem1  29434  elfuns  29537  brimg  29559  brsuccf  29563  dfrdg4  29572  tfrqfree  29573  brofs  29627  funtransport  29653  fvtransport  29654  brifs  29665  lineext  29698  brfs  29701  btwnconn1lem11  29719  btwnconn1lem14  29722  brsegle  29730  segletr  29736  segleantisym  29737  seglelin  29738  funray  29762  fvray  29763  funline  29764  fvline  29766  ellines  29774  linethru  29775  ptrest  30020  mblfinlem3  30025  mblfinlem4  30026  ismblfin  30027  mbfresfi  30033  itg2addnclem  30038  itg2addnclem3  30040  itg2addnc  30041  ftc1anclem7  30068  ftc1anc  30070  areacirclem5  30083  trer  30106  opnrebl2  30111  nn0prpwlem  30112  isfne4  30130  isfne2  30132  isfne3  30133  unirep  30175  fnopabeqd  30182  fdc  30210  fdc1  30211  istotbnd  30237  heibor1lem  30277  heibor  30289  isriscg  30359  iscringd  30368  isidlc  30384  prtlem16  30582  prtlem15  30588  ismrcd1  30602  ismrcd2  30603  mzpcompact2lem  30656  eldioph  30663  eldioph2  30667  eldioph2b  30668  eldioph3  30671  diophin  30678  diophun  30679  diophrex  30681  rexrabdioph  30699  fphpd  30722  fphpdo  30723  pellexlem3  30739  monotuz  30849  monotoddzzfi  30850  monotoddzz  30851  oddcomabszz  30852  jm2.27  30922  rmydioph  30928  expdiophlem1  30935  expdiophlem2  30936  aomclem6  30977  aomclem8  30979  islssfg  30988  islssfg2  30989  hbtlem2  31045  hbtlem4  31047  hbtlem5  31049  hbtlem6  31050  dgraaval  31066  flcidc  31096  dvgrat  31166  cvgdvgrat  31167  lcmval  31171  lcmneg  31182  lcmgcdlem  31185  lcmass  31191  2sbc6g  31273  2sbc5g  31274  iotasbc2  31278  pm14.122a  31280  pm14.123a  31283  monoords  31445  fperiodmullem  31452  fmul01  31502  fmuldfeqlem1  31504  fmuldfeq  31505  fmul01lt1lem1  31506  fmul01lt1lem2  31507  climmulf  31518  climexp  31519  climsuse  31522  climrecf  31523  climinff  31525  climaddf  31529  mullimc  31530  limcdm0  31532  climf  31536  mullimcf  31537  constlimc  31538  idlimc  31540  limcperiod  31542  sumnnodd  31544  clim2f  31550  limcleqr  31558  neglimc  31561  addlimc  31562  0ellimcdiv  31563  cncfshift  31583  cncfperiod  31588  icccncfext  31597  fperdvper  31619  ioodvbdlimc1lem2  31633  ioodvbdlimc2lem  31635  iblspltprt  31662  itgspltprt  31668  stoweidlem3  31674  stoweidlem4  31675  stoweidlem7  31678  stoweidlem15  31686  stoweidlem16  31687  stoweidlem17  31688  stoweidlem19  31690  stoweidlem20  31691  stoweidlem22  31693  stoweidlem23  31694  stoweidlem27  31698  stoweidlem30  31701  stoweidlem32  31703  stoweidlem34  31705  stoweidlem42  31713  stoweidlem43  31714  stoweidlem48  31719  stoweidlem51  31722  stoweidlem59  31730  stoweidlem60  31731  dirkercncflem2  31775  fourierdlem2  31780  fourierdlem3  31781  fourierdlem11  31789  fourierdlem12  31790  fourierdlem15  31793  fourierdlem16  31794  fourierdlem21  31799  fourierdlem34  31812  fourierdlem41  31819  fourierdlem42  31820  fourierdlem46  31824  fourierdlem48  31826  fourierdlem49  31827  fourierdlem50  31828  fourierdlem51  31829  fourierdlem54  31832  fourierdlem68  31846  fourierdlem71  31849  fourierdlem72  31850  fourierdlem73  31851  fourierdlem76  31854  fourierdlem79  31857  fourierdlem81  31859  fourierdlem83  31861  fourierdlem86  31864  fourierdlem87  31865  fourierdlem89  31867  fourierdlem90  31868  fourierdlem91  31869  fourierdlem92  31870  fourierdlem94  31872  fourierdlem97  31875  fourierdlem103  31881  fourierdlem104  31882  fourierdlem107  31885  fourierdlem111  31889  fourierdlem112  31890  fourierdlem113  31891  2reu4a  32032  isfusgracl  32264  rngcinv  32526  rngcinvOLD  32538  ringcinv  32572  ringcinvOLD  32596  opeliun2xp  32650  mpt2mptx2  32652  lcoval  32743  lco0  32758  islinindfis  32780  snlindsntor  32802  bnj976  33564  bnj852  33707  bnj1014  33746  bnj1015  33747  bnj1118  33768  bnj1123  33770  bnj1148  33780  bnj1171  33784  bnj1373  33814  bnj1489  33840  bj-eleq2w  34156  bj-finsumval0  34386  fsumshftd  34405  fsumshftdOLD  34406  lsmsat  34456  lsmsatcv  34458  islshpat  34465  lcvfbr  34468  lcvbr  34469  lsatcv0  34479  islshpkrN  34568  cvrval  34717  cvrval2  34722  cvrnbtwn2  34723  cvlexch1  34776  hlsuprexch  34828  cvrval5  34862  cvrat  34869  cvrat42  34891  3dim0  34904  3dim2  34915  islpln3  34980  islpln5  34982  islvol3  35023  islvol5  35026  4atlem11  35056  lineset  35185  isline  35186  ispsubsp2  35193  isline2  35221  isline3  35223  elpaddat  35251  elpadd2at  35253  dalawlem15  35332  pclfinclN  35397  4atex  35523  4atex2  35524  4atex3  35528  ltrnu  35568  cdleme0nex  35738  cdleme31so  35828  cdleme31fv  35839  cdleme31fv2  35842  cdlemefrs29pre00  35844  cdlemefrs29cpre1  35847  cdlemftr3  36014  cdlemb3  36055  cdlemg6d  36070  cdlemg33b  36156  cdlemg33c  36157  cdlemg33e  36159  cdlemk42  36390  dvhopellsm  36567  dibelval3  36597  diblsmopel  36621  diclspsn  36644  dihval  36682  dihopelvalcpre  36698  dih1dimatlem  36779  dihglb2  36792  dochkrshp3  36838  dihjatcclem4  36871  dihjat1lem  36878  mapdval  37078  mapdpglem30  37152  dfhe3  37469
  Copyright terms: Public domain W3C validator