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  2394  eleq2dALT  2538  eleq2OLD  2542  ceqsex2  3151  ceqsex6v  3155  vtocl2gaf  3178  vtocl4ga  3183  ceqsrex2v  3239  moeq3  3280  mob2  3283  eqreu  3295  reu2eqd  3300  nelrdva  3313  undif4  3883  r19.27z  3926  r19.27zv  3927  ssunsn2  4186  preq12bg  4205  prel12g  4206  opeq2  4214  ralunsn  4233  intab  4312  disjxun  4445  opabbid  4509  opthg  4722  pocl  4807  isso2i  4832  ordelord  4900  ordtri4  4915  xpeq2  5014  rabxp  5035  vtoclr  5043  opeliunxp  5050  posn  5067  opbrop  5077  elrnmpt1  5249  dfres2  5324  brcodir  5384  poltletr  5400  xp11  5440  fununi  5652  fneq2  5668  fnun  5685  feq3  5713  foeq3  5791  funbrfv  5904  ssimaexg  5931  fvopab3g  5944  fvopab3ig  5945  fvelrn  6015  fvcofneq  6027  fmptco  6052  elunirn  6149  f12dfv  6165  f13dfv  6166  isoeq2  6202  isoeq3  6203  isoini  6220  isopolem  6227  f1oiso  6233  f1oiso2  6234  oprabv  6327  oprabbid  6332  cbvoprab3  6355  mpt2mptx  6375  mpt2fun  6386  elrnmpt2res  6398  ov  6404  ov3  6421  ov6g  6422  ovg  6423  caoftrn  6557  dfwe2  6595  dflim4  6661  tfisi  6671  elxp4  6725  elxp5  6726  f1o2ndf1  6888  frxp  6890  xporderlem  6891  fnwelem  6895  brtpos2  6958  dftpos4  6971  onfununi  7009  recseq  7040  omopth  7304  brecop  7401  eroveu  7403  erovlem  7404  erov  7405  ecopovtrn  7411  elpmg  7431  ixpsnval  7469  ixpsnf1o  7506  domeng  7527  dom2lem  7552  xpcomco  7604  xpassen  7608  xpdom2  7609  omxpenlem  7615  xpf1o  7676  unxpdom  7724  isinf  7730  findcard2  7756  findcard2d  7758  fiint  7793  supeq2  7904  wemapso2lem  7974  inf0  8034  cantnfp1lem3  8095  cantnfp1  8096  scott0  8300  isinffi  8369  isacn  8421  aceq1  8494  aceq0  8495  aceq2  8496  dfac3  8498  dfac5lem1  8500  dfac2  8507  dfac12lem2  8520  kmlem8  8533  kmlem14  8539  infmap2  8594  cfval  8623  cflim3  8638  sornom  8653  infpssrlem4  8682  isf32lem9  8737  domtriomlem  8818  axdc2lem  8824  zfac  8836  ac6num  8855  axrepndlem1  8963  axunndlem1  8966  axregnd  8977  axregndOLD  8978  axinfndlem1  8979  axacndlem4  8984  axacndlem5  8985  zfcndac  8993  fpwwe2lem5  9008  pwfseqlem4a  9035  pwfseqlem4  9036  alephgch  9048  wunex2  9112  tskord  9154  nqereu  9303  ordpipq  9316  prcdnq  9367  prnmax  9369  genpnnp  9379  distrlem5pr  9401  ltprord  9404  ltexprlem3  9412  ltexprlem4  9413  ltexpri  9417  prlem936  9421  reclem2pr  9422  addsrmo  9446  mulsrmo  9447  addsrpr  9448  mulsrpr  9449  ltsosr  9467  mulgt0sr  9478  ltresr  9513  axpre-lttrn  9539  axpre-mulgt0  9541  eqlelt  9668  lesub0  10065  wloglei  10081  mulle0b  10409  sup3  10496  infm3  10498  prime  10937  fzind  10955  uzwo  11140  uzwoOLD  11141  zbtwnre  11176  xltnegi  11411  xmulneg1  11457  ixxval  11533  fzval  11670  elfzm11  11745  elfzo  11795  seqof2  12129  nn0opth2  12316  facwordi  12331  hashnn0n0nn  12422  brfi1uzind  12494  wrdeqswrdlsw  12633  2swrd1eqwrdeq  12638  wrd2ind  12662  cshwcsh2id  12755  2swrd2eqwrdeq  12850  shftfval  12862  shftfib  12864  shftfn  12865  2shfti  12872  abs1m  13127  cau3lem  13146  caubnd2  13149  clim  13276  rlim  13277  clim2  13286  climi  13292  o1lo1  13319  rlimcn2  13372  climcn2  13374  addcn2  13375  subcn2  13376  mulcn2  13377  o1of2  13394  isercoll  13449  caurcvg2  13459  sumeq2w  13473  sumeq2ii  13474  summo  13498  fsum  13501  sinbnd  13772  cosbnd  13773  divalgb  13917  ndvdssub  13920  smupp1  13985  smueqlem  13995  gcdval  14001  gcdcllem2  14005  gcdneg  14019  gcdass  14038  algcvgblem  14061  prmind2  14083  qredeq  14102  euclemma  14104  qnumval  14125  qdenval  14126  eulerthlem2  14167  pceu  14225  pczpre  14226  pcdiv  14231  prmpwdvds  14277  prmreclem5  14293  vdwapun  14347  ramub2  14387  rami  14388  ramcl  14402  ismred2  14854  isacs  14902  iscatd2  14932  catpropd  14961  oppccatid  14971  isinv  15011  isssc  15046  funcres2b  15120  funcpropd  15123  fucinv  15196  yoniso  15408  prslem  15414  drsdir  15418  drsdirfi  15421  posi  15433  isposd  15438  pltval  15443  plttr  15453  isipodrs  15644  ipodrsima  15648  dirge  15720  mndlem1  15732  mrcmndind  15807  gsumpropd  15817  gsumress  15820  divsgrp2  15988  resscntz  16164  psgnunilem3  16317  psgneu  16327  psgnvali  16329  psgnvalii  16330  isslw  16424  subgslw  16432  iscmnd  16606  gsumval3eu  16698  gsumval3OLD  16699  gsumval3lem2  16701  telgsumfzs  16809  dmdprd  16820  subgdmdprd  16871  dprd2d2  16883  pgpfac1  16921  pgpfaclem2  16923  pgpfaclem3  16924  pgpfac  16925  ablfaclem1  16926  divsrng2  17053  dvdsrval  17078  crngunit  17095  dfrhm2  17150  isdrngd  17204  abvpropd  17274  islmod  17299  lssacs  17396  lsspropd  17446  islmhm  17456  lbspropd  17528  ixpsnbasval  17638  fiidomfld  17728  ltbval  17907  opsrval  17910  mpfind  17976  coe1fzgsumd  18115  pf1ind  18162  evl1gsumd  18164  psgndiflemA  18404  pjfval2  18507  frlmup1  18599  scmatf1  18800  mdetralt  18877  mdetralt2  18878  mdetunilem1  18881  mdetunilem2  18882  mdetunilem9  18889  gsummatr01  18928  eltopspOLD  19186  istpsOLD  19188  basis2  19219  eltg2  19226  isclo  19354  isnei  19370  isneip  19372  neiptopnei  19399  restbas  19425  restcld  19439  neitr  19447  iscnp  19504  iscnp3  19511  tgcn  19519  cnpimaex  19523  lmbrf  19527  cncnp  19547  cnprest2  19557  isreg  19599  regsep  19601  isnrm  19602  ist1-2  19614  nrmsep3  19622  isnrm2  19625  hauscmplem  19672  dfcon2  19686  is1stc  19708  1stcclb  19711  1stcfb  19712  is2ndc  19713  2ndc1stc  19718  1stcrest  19720  2ndcsep  19726  1stccnp  19729  islly  19735  llyeq  19737  llyi  19741  hausllycmp  19761  lly1stc  19763  txbas  19803  ptpjpre1  19807  elpt  19808  txcnpi  19844  ptpjopn  19848  ptcldmpt  19850  ptclsg  19851  txcnp  19856  ptcnp  19858  hausdiag  19881  tx1stc  19886  xkoinjcn  19923  imasnopn  19926  imasncld  19927  imasncls  19928  fbfinnfr  20077  snfil  20100  uffix2  20160  elfm  20183  elfm2  20184  fmco  20197  hauspwpwf1  20223  flfnei  20227  isflf  20229  lmflf  20241  fclscf  20261  isfcf  20270  alexsublem  20279  cnextcn  20302  cnextfres  20303  eltsms  20366  tsmsresOLD  20380  tsmsres  20381  tsmsf1o  20382  ustuqtop4  20482  ispsmet  20543  ismet  20561  isxmet  20562  ismet2  20571  imasdsf1olem  20611  blres  20669  met2ndc  20761  metcnp3  20778  nrmmetd  20830  pi1grplem  21284  lmmbr2  21433  lmmbrf  21436  iscau2  21451  iscau4  21453  caucfil  21457  lmclim  21476  cfilucfil3OLD  21492  cfilucfil3  21493  bcthlem1  21498  bcth  21503  ishl2  21545  pmltpclem1  21595  elovolm  21621  ovolgelb  21626  ovolicc  21669  mbfaddlem  21802  i1fres  21847  mbfi1fseqlem4  21860  itg2l  21871  itg2leub  21876  itg2seq  21884  isibl  21907  iblitg  21910  dfitg  21911  itgeq2  21919  itgvallem  21926  iblcnlem1  21929  iblrelem  21932  iblpos  21934  ellimc3  22018  limciun  22033  limcun  22034  dvmptfsum  22111  dveflem  22115  lhop1lem  22149  dvfsumlem2  22163  dvfsumlem4  22165  mdegleb  22199  elply2  22328  plypf1  22344  coeval  22355  plydivlem4  22426  sincosq3sgn  22626  vmasum  23219  lgsqrlem1  23344  lgsquadlem1  23357  2sqlem8  23375  2sqlem9  23376  2sqlem11  23378  dchrisumlema  23401  dchrisumlem2  23403  pntibndlem3  23505  pntibnd  23506  pntleme  23521  pntlemp  23523  axtgsegcon  23589  axtg5seg  23590  axtgpasch  23592  iscgrg  23632  legov  23699  ltgov  23710  mirreu3  23748  brcgr  23879  brbtwn2  23884  colinearalg  23889  ax5seg  23917  axcontlem5  23947  axcontlem10  23952  usgraedg4  24063  cusgrafilem2  24156  cusgrafi  24158  uvtx01vtx  24168  usgrnloop  24241  spthonepeq  24265  usgra2adedgwlkonALT  24292  usgra2wlkspthlem1  24295  usgrcyclnl2  24317  4cycl4v4e  24342  4cycl4dv4e  24344  wwlk  24357  wlklniswwlkn2  24376  clwlkisclwwlklem0  24464  clwlkisclwwlk  24465  eleclclwwlkn  24509  usghashecclwwlk  24511  el2wlkonot  24545  el2spthonot  24546  el2spthonot0  24547  usg2spthonot  24564  usg2spthonot0  24565  usg2spthonot1  24566  isrusgra  24603  isrusgusrg  24608  isrgrac  24610  isrusgrac  24611  rusgranumwlkl1  24623  iseupa  24641  eupath2lem3  24655  1vwmgra  24679  3vfriswmgra  24681  3cyclfrgrarn1  24688  4cycl2vnunb  24693  vdn1frgrav2  24702  vdgn1frgrav2  24703  frgrancvvdeqlemB  24715  usg2spot2nb  24742  usgreg2spot  24744  2spotmdisj  24745  usgreghash2spot  24746  extwwlkfab  24767  numclwwlk2lem1  24779  numclwwlk5  24789  isgrpo  24874  isgrp2d  24913  isgrpda  24975  ismndo  25021  drngoi  25085  vci  25117  isvclem  25146  nmoofval  25353  nmooval  25354  nmosetn0  25356  nmoolb  25362  nmoubi  25363  nmoo0  25382  nmlno0lem  25384  isphg  25408  norm3lemt  25745  chlimi  25828  ocsh  25877  cmbr  26178  chscllem2  26232  spansncv  26247  eigorth  26433  nmopval  26451  nmopsetn0  26460  nmfnval  26471  nmfnsetn0  26473  nmoplb  26502  nmfnlb  26519  nmopnegi  26560  nmop0  26581  nmfn0  26582  nmlnop0iALT  26590  nmopun  26609  nmcexi  26621  branmfn  26700  leopmuli  26728  pjnmopi  26743  cvbr  26877  mdbr  26889  dmdbr  26894  atom1d  26948  chrelat2  26965  atcvati  26981  atord  26983  atcvat2  26984  chirredlem4  26988  mdsymlem5  27002  disjunsn  27126  opeldifid  27129  fcoinvbr  27134  fmptcof2  27174  ofpreima  27179  funcnv4mpt  27184  mpt2mptxf  27190  2ndpreima  27197  f1od2  27219  xeqlelt  27255  ishashinf  27274  ressprs  27305  isomnd  27353  archiabllem2a  27400  archiabl  27404  isslmd  27407  gsumle  27433  gsumvsca1  27436  gsumvsca2  27437  ismntop  27644  esumcvg  27732  sitgval  27914  eulerpartlemmf  27954  eulerpartlemgvv  27955  eulerpartlemn  27960  eulerpart  27961  brafs  28192  lgamgulmlem2  28212  erdszelem3  28277  erdsze  28286  pconcn  28309  cnpcon  28315  txpcon  28317  conpcon  28320  cvmscbv  28343  iscvm  28344  cvmsi  28350  cvmsval  28351  relexp0  28527  relexpsucr  28528  relexpsucl  28530  relexpadd  28536  relexpindlem  28537  prodfdiv  28607  ntrivcvgn0  28609  ntrivcvgmullem  28612  prodeq1f  28617  prodeq2w  28621  prodeq2ii  28622  prodmo  28645  zprod  28646  fprod  28650  fprodntriv  28651  elima4  28786  dfrdg2  28805  dfrdg3  28806  elpred  28834  trpredrec  28898  poseq  28910  soseq  28911  sltval  28984  nocvxminlem  29027  nofulllem1  29039  elfuns  29142  brimg  29164  brsuccf  29168  dfrdg4  29177  tfrqfree  29178  brofs  29232  funtransport  29258  fvtransport  29259  brifs  29270  lineext  29303  brfs  29306  btwnconn1lem11  29324  btwnconn1lem14  29327  brsegle  29335  segletr  29341  segleantisym  29342  seglelin  29343  funray  29367  fvray  29368  funline  29369  fvline  29371  ellines  29379  linethru  29380  ptrest  29625  mblfinlem3  29630  mblfinlem4  29631  ismblfin  29632  mbfresfi  29638  itg2addnclem  29643  itg2addnclem3  29645  itg2addnc  29646  ftc1anclem7  29673  ftc1anc  29675  areacirclem5  29688  trer  29711  opnrebl2  29716  nn0prpwlem  29717  isfne4  29741  isfne2  29743  isfne3  29744  islocfin  29768  unirep  29806  fnopabeqd  29813  fdc  29841  fdc1  29842  istotbnd  29868  heibor1lem  29908  heibor  29920  isriscg  29990  iscringd  29999  isidlc  30015  prtlem16  30214  prtlem15  30220  ismrcd1  30234  ismrcd2  30235  mzpcompact2lem  30288  eldioph  30295  eldioph2  30299  eldioph2b  30300  eldioph3  30303  diophin  30310  diophun  30311  diophrex  30313  rexrabdioph  30331  fphpd  30354  fphpdo  30355  pellexlem3  30371  monotuz  30481  monotoddzzfi  30482  monotoddzz  30483  oddcomabszz  30484  jm2.27  30554  rmydioph  30560  expdiophlem1  30567  expdiophlem2  30568  aomclem6  30609  aomclem8  30611  islssfg  30620  islssfg2  30621  hbtlem2  30677  hbtlem4  30679  hbtlem5  30681  hbtlem6  30682  dgraaval  30698  flcidc  30728  lcmval  30798  lcmneg  30809  lcmgcdlem  30812  lcmass  30818  2sbc6g  30900  2sbc5g  30901  iotasbc2  30905  pm14.122a  30907  pm14.123a  30910  monoords  31073  fperiodmullem  31080  fmul01  31130  fmuldfeqlem1  31132  fmuldfeq  31133  fmul01lt1lem1  31134  fmul01lt1lem2  31135  climmulf  31146  climexp  31147  climsuse  31150  climrecf  31151  climinff  31153  climaddf  31157  mullimc  31158  limcdm0  31160  climf  31164  mullimcf  31165  constlimc  31166  idlimc  31168  limcperiod  31170  sumnnodd  31172  clim2f  31178  limcleqr  31186  neglimc  31189  addlimc  31190  0ellimcdiv  31191  cncfshift  31212  cncfperiod  31217  icccncfext  31226  fperdvper  31248  ioodvbdlimc1lem2  31262  ioodvbdlimc2lem  31264  iblspltprt  31291  itgspltprt  31297  stoweidlem3  31303  stoweidlem4  31304  stoweidlem7  31307  stoweidlem15  31315  stoweidlem16  31316  stoweidlem17  31317  stoweidlem19  31319  stoweidlem20  31320  stoweidlem22  31322  stoweidlem23  31323  stoweidlem27  31327  stoweidlem30  31330  stoweidlem32  31332  stoweidlem34  31334  stoweidlem42  31342  stoweidlem43  31343  stoweidlem48  31348  stoweidlem51  31351  stoweidlem59  31359  stoweidlem60  31360  dirkercncflem2  31404  fourierdlem2  31409  fourierdlem3  31410  fourierdlem11  31418  fourierdlem12  31419  fourierdlem15  31422  fourierdlem16  31423  fourierdlem21  31428  fourierdlem34  31441  fourierdlem41  31448  fourierdlem42  31449  fourierdlem46  31453  fourierdlem48  31455  fourierdlem49  31456  fourierdlem50  31457  fourierdlem51  31458  fourierdlem54  31461  fourierdlem68  31475  fourierdlem71  31478  fourierdlem72  31479  fourierdlem73  31480  fourierdlem76  31483  fourierdlem79  31486  fourierdlem81  31488  fourierdlem83  31490  fourierdlem86  31493  fourierdlem87  31494  fourierdlem89  31496  fourierdlem90  31497  fourierdlem91  31498  fourierdlem92  31499  fourierdlem94  31501  fourierdlem97  31504  fourierdlem103  31510  fourierdlem104  31511  fourierdlem107  31514  fourierdlem111  31518  fourierdlem112  31519  fourierdlem113  31520  2reu4a  31661  isfusgracl  31895  opeliun2xp  31986  mpt2mptx2  31988  lcoval  32086  lco0  32101  islinindfis  32123  snlindsntor  32145  mnd1  32161  bnj976  32915  bnj852  33058  bnj1014  33097  bnj1015  33098  bnj1118  33119  bnj1123  33121  bnj1148  33131  bnj1171  33135  bnj1373  33165  bnj1489  33191  bj-eleq2w  33504  bj-finsumval0  33735  fsumshftd  33754  fsumshftdOLD  33755  lsmsat  33805  lsmsatcv  33807  islshpat  33814  lcvfbr  33817  lcvbr  33818  lsatcv0  33828  islshpkrN  33917  cvrval  34066  cvrval2  34071  cvrnbtwn2  34072  cvlexch1  34125  hlsuprexch  34177  cvrval5  34211  cvrat  34218  cvrat42  34240  3dim0  34253  3dim2  34264  islpln3  34329  islpln5  34331  islvol3  34372  islvol5  34375  4atlem11  34405  lineset  34534  isline  34535  ispsubsp2  34542  isline2  34570  isline3  34572  elpaddat  34600  elpadd2at  34602  dalawlem15  34681  pclfinclN  34746  4atex  34872  4atex2  34873  4atex3  34877  ltrnu  34917  cdleme0nex  35086  cdleme31so  35175  cdleme31fv  35186  cdleme31fv2  35189  cdlemefrs29pre00  35191  cdlemefrs29cpre1  35194  cdlemftr3  35361  cdlemb3  35402  cdlemg6d  35417  cdlemg33b  35503  cdlemg33c  35504  cdlemg33e  35506  cdlemk42  35737  dvhopellsm  35914  dibelval3  35944  diblsmopel  35968  diclspsn  35991  dihval  36029  dihopelvalcpre  36045  dih1dimatlem  36126  dihglb2  36139  dochkrshp3  36185  dihjatcclem4  36218  dihjat1lem  36225  mapdval  36425  mapdpglem30  36499
  Copyright terms: Public domain W3C validator