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  868  2eu6OLD  2379  eleq2dALT  2522  eleq2OLD  2526  ceqsex2  3106  ceqsex6v  3110  vtocl2gaf  3133  vtocl4ga  3138  ceqsrex2v  3192  moeq3  3233  mob2  3236  eqreu  3248  reu2eqd  3253  nelrdva  3266  undif4  3833  r19.27z  3876  r19.27zv  3877  ssunsn2  4130  preq12bg  4149  prel12g  4150  opeq2  4158  ralunsn  4177  intab  4256  disjxun  4388  opabbid  4452  opthg  4665  pocl  4746  isso2i  4771  ordelord  4839  ordtri4  4854  xpeq2  4953  rabxp  4973  vtoclr  4981  opeliunxp  4988  posn  5005  opbrop  5014  elrnmpt1  5186  dfres2  5256  brcodir  5315  poltletr  5331  xp11  5371  fununi  5582  fneq2  5598  fnun  5615  feq3  5642  foeq3  5716  funbrfv  5829  ssimaexg  5856  fvopab3g  5869  fvopab3ig  5870  fvelrn  5938  fvcofneq  5950  fmptco  5975  elunirn  6067  isoeq2  6110  isoeq3  6111  isoini  6128  isopolem  6135  f1oiso  6141  f1oiso2  6142  oprabbid  6238  cbvoprab3  6261  mpt2mptx  6281  mpt2fun  6292  elrnmpt2res  6304  ov  6310  ov3  6327  ov6g  6328  ovg  6329  caoftrn  6455  dfwe2  6493  dflim4  6559  tfisi  6569  elxp4  6622  elxp5  6623  f1o2ndf1  6780  frxp  6782  xporderlem  6783  fnwelem  6787  brtpos2  6851  dftpos4  6864  onfununi  6902  recseq  6933  omopth  7197  brecop  7293  eroveu  7295  erovlem  7296  erov  7297  ecopovtrn  7303  th3qlem1  7306  th3qlem2  7307  th3q  7309  elpmg  7328  ixpsnval  7366  ixpsnf1o  7403  domeng  7424  dom2lem  7449  xpcomco  7501  xpassen  7505  xpdom2  7506  omxpenlem  7512  xpf1o  7573  unxpdom  7621  isinf  7627  findcard2  7653  findcard2d  7655  fiint  7689  supeq2  7799  wemapso2lem  7868  inf0  7928  cantnfp1lem3  7989  cantnfp1  7990  scott0  8194  isinffi  8263  isacn  8315  aceq1  8388  aceq0  8389  aceq2  8390  dfac3  8392  dfac5lem1  8394  dfac2  8401  dfac12lem2  8414  kmlem8  8427  kmlem14  8433  infmap2  8488  cfval  8517  cflim3  8532  sornom  8547  infpssrlem4  8576  isf32lem9  8631  domtriomlem  8712  axdc2lem  8718  zfac  8730  ac6num  8749  axrepndlem1  8857  axunndlem1  8860  axregnd  8871  axregndOLD  8872  axinfndlem1  8873  axacndlem4  8878  axacndlem5  8879  zfcndac  8887  fpwwe2lem5  8902  pwfseqlem4a  8929  pwfseqlem4  8930  alephgch  8942  wunex2  9006  tskord  9048  nqereu  9199  ordpipq  9212  prcdnq  9263  prnmax  9265  genpnnp  9275  distrlem5pr  9297  ltprord  9300  ltexprlem3  9308  ltexprlem4  9309  ltexpri  9313  prlem936  9317  reclem2pr  9318  ltsosr  9362  mulgt0sr  9373  ltresr  9408  axpre-lttrn  9434  axpre-mulgt0  9436  eqlelt  9563  lesub0  9957  wloglei  9973  mulle0b  10301  sup3  10388  infm3  10390  prime  10823  fzind  10841  uzwo  11018  uzwoOLD  11019  zbtwnre  11052  xltnegi  11287  xmulneg1  11333  ixxval  11409  fzval  11540  elfzm11  11629  elfzo  11656  seqof2  11965  nn0opth2  12151  facwordi  12166  hashnn0n0nn  12255  brfi1uzind  12321  wrdeqswrdlsw  12445  2swrd1eqwrdeq  12450  wrd2ind  12474  2swrd2eqwrdeq  12655  shftfval  12661  shftfib  12663  shftfn  12664  2shfti  12671  abs1m  12925  cau3lem  12944  caubnd2  12947  clim  13074  rlim  13075  clim2  13084  climi  13090  o1lo1  13117  rlimcn2  13170  climcn2  13172  addcn2  13173  subcn2  13174  mulcn2  13175  o1of2  13192  isercoll  13247  caurcvg2  13257  sumeq2w  13271  sumeq2ii  13272  summo  13296  fsum  13299  sinbnd  13566  cosbnd  13567  divalgb  13710  ndvdssub  13713  smupp1  13778  smueqlem  13788  gcdval  13794  gcdcllem2  13798  gcdneg  13812  gcdass  13831  algcvgblem  13854  prmind2  13876  qredeq  13894  euclemma  13896  qnumval  13917  qdenval  13918  eulerthlem2  13959  pceu  14015  pczpre  14016  pcdiv  14021  prmpwdvds  14067  prmreclem5  14083  vdwapun  14137  ramub2  14177  rami  14178  ramcl  14192  ismred2  14643  isacs  14691  iscatd2  14721  catpropd  14750  oppccatid  14760  isinv  14800  isssc  14835  funcres2b  14909  funcpropd  14912  fucinv  14985  yoniso  15197  prslem  15203  drsdir  15207  drsdirfi  15210  posi  15222  isposd  15227  pltval  15232  plttr  15242  isipodrs  15433  ipodrsima  15437  dirge  15509  mndlem1  15521  mrcmndind  15596  gsumpropd  15606  gsumress  15609  divsgrp2  15775  resscntz  15951  psgnunilem3  16104  psgneu  16114  psgnvali  16116  psgnvalii  16117  isslw  16211  subgslw  16219  iscmnd  16393  gsumval3eu  16485  gsumval3OLD  16486  gsumval3lem2  16488  dmdprd  16585  subgdmdprd  16636  dprd2d2  16648  pgpfac1  16686  pgpfaclem2  16688  pgpfaclem3  16689  pgpfac  16690  ablfaclem1  16691  divsrng2  16818  dvdsrval  16843  crngunit  16860  dfrhm2  16914  isdrngd  16963  abvpropd  17033  islmod  17058  lssacs  17154  lsspropd  17204  islmhm  17214  lbspropd  17286  ixpsnbasval  17396  fiidomfld  17486  ltbval  17660  opsrval  17663  mpfind  17729  pf1ind  17898  evl1gsumd  17900  psgndiflemA  18140  pjfval2  18243  frlmup1  18335  mdetralt  18530  mdetralt2  18531  mdetunilem1  18534  mdetunilem2  18535  mdetunilem9  18542  gsummatr01  18581  eltopspOLD  18639  istpsOLD  18641  basis2  18672  eltg2  18679  isclo  18807  isnei  18823  isneip  18825  neiptopnei  18852  restbas  18878  restcld  18892  neitr  18900  iscnp  18957  iscnp3  18964  tgcn  18972  cnpimaex  18976  lmbrf  18980  cncnp  19000  cnprest2  19010  isreg  19052  regsep  19054  isnrm  19055  ist1-2  19067  nrmsep3  19075  isnrm2  19078  hauscmplem  19125  dfcon2  19139  is1stc  19161  1stcclb  19164  1stcfb  19165  is2ndc  19166  2ndc1stc  19171  1stcrest  19173  2ndcsep  19179  1stccnp  19182  islly  19188  llyeq  19190  llyi  19194  hausllycmp  19214  lly1stc  19216  txbas  19256  ptpjpre1  19260  elpt  19261  txcnpi  19297  ptpjopn  19301  ptcldmpt  19303  ptclsg  19304  txcnp  19309  ptcnp  19311  hausdiag  19334  tx1stc  19339  xkoinjcn  19376  imasnopn  19379  imasncld  19380  imasncls  19381  fbfinnfr  19530  snfil  19553  uffix2  19613  elfm  19636  elfm2  19637  fmco  19650  hauspwpwf1  19676  flfnei  19680  isflf  19682  lmflf  19694  fclscf  19714  isfcf  19723  alexsublem  19732  cnextcn  19755  cnextfres  19756  eltsms  19819  tsmsresOLD  19833  tsmsres  19834  tsmsf1o  19835  ustuqtop4  19935  ispsmet  19996  ismet  20014  isxmet  20015  ismet2  20024  imasdsf1olem  20064  blres  20122  met2ndc  20214  metcnp3  20231  nrmmetd  20283  pi1grplem  20737  lmmbr2  20886  lmmbrf  20889  iscau2  20904  iscau4  20906  caucfil  20910  lmclim  20929  cfilucfil3OLD  20945  cfilucfil3  20946  bcthlem1  20951  bcth  20956  ishl2  20998  pmltpclem1  21048  elovolm  21074  ovolgelb  21079  ovolicc  21122  mbfaddlem  21254  i1fres  21299  mbfi1fseqlem4  21312  itg2l  21323  itg2leub  21328  itg2seq  21336  isibl  21359  iblitg  21362  dfitg  21363  itgeq2  21371  itgvallem  21378  iblcnlem1  21381  iblrelem  21384  iblpos  21386  ellimc3  21470  limciun  21485  limcun  21486  dvmptfsum  21563  dveflem  21567  lhop1lem  21601  dvfsumlem2  21615  dvfsumlem4  21617  mdegleb  21651  elply2  21780  plypf1  21796  coeval  21807  plydivlem4  21878  sincosq3sgn  22078  vmasum  22671  lgsqrlem1  22796  lgsquadlem1  22809  2sqlem8  22827  2sqlem9  22828  2sqlem11  22830  dchrisumlema  22853  dchrisumlem2  22855  pntibndlem3  22957  pntibnd  22958  pntleme  22973  pntlemp  22975  axtgsegcon  23041  axtg5seg  23042  axtgpasch  23044  iscgrg  23084  legov  23137  mirreu3  23184  brcgr  23281  brbtwn2  23286  colinearalg  23291  ax5seg  23319  axcontlem5  23349  axcontlem10  23354  usgraedg4  23440  cusgrafilem2  23523  cusgrafi  23525  uvtx01vtx  23535  usgrnloop  23597  spthonepeq  23621  usgrcyclnl2  23662  4cycl4v4e  23687  4cycl4dv4e  23689  iseupa  23721  eupath2lem3  23735  isgrpo  23818  isgrp2d  23857  isgrpda  23919  ismndo  23965  drngoi  24029  vci  24061  isvclem  24090  nmoofval  24297  nmooval  24298  nmosetn0  24300  nmoolb  24306  nmoubi  24307  nmoo0  24326  nmlno0lem  24328  isphg  24352  norm3lemt  24689  chlimi  24772  ocsh  24821  cmbr  25122  chscllem2  25176  spansncv  25191  eigorth  25377  nmopval  25395  nmopsetn0  25404  nmfnval  25415  nmfnsetn0  25417  nmoplb  25446  nmfnlb  25463  nmopnegi  25504  nmop0  25525  nmfn0  25526  nmlnop0iALT  25534  nmopun  25553  nmcexi  25565  branmfn  25644  leopmuli  25672  pjnmopi  25687  cvbr  25821  mdbr  25833  dmdbr  25838  atom1d  25892  chrelat2  25909  atcvati  25925  atord  25927  atcvat2  25928  chirredlem4  25932  mdsymlem5  25946  disjunsn  26070  fmptcof2  26113  ofpreima  26118  funcnv4mpt  26123  mpt2mptxf  26129  2ndpreima  26136  f1od2  26158  xeqlelt  26200  ishashinf  26219  ressprs  26250  isomnd  26298  archiabllem2a  26345  archiabl  26349  isslmd  26352  gsumle  26380  gsumvsca1  26385  gsumvsca2  26386  esumcvg  26669  sitgval  26852  eulerpartlemmf  26892  eulerpartlemgvv  26893  eulerpartlemn  26898  eulerpart  26899  brafs  27130  lgamgulmlem2  27150  erdszelem3  27215  erdsze  27224  pconcn  27247  cnpcon  27253  txpcon  27255  conpcon  27258  cvmscbv  27281  iscvm  27282  cvmsi  27288  cvmsval  27289  relexp0  27465  relexpsucr  27466  relexpsucl  27468  relexpadd  27474  relexpindlem  27475  prodfdiv  27545  ntrivcvgn0  27547  ntrivcvgmullem  27550  prodeq1f  27555  prodeq2w  27559  prodeq2ii  27560  prodmo  27583  zprod  27584  fprod  27588  fprodntriv  27589  elima4  27724  dfrdg2  27743  dfrdg3  27744  elpred  27772  trpredrec  27836  poseq  27848  soseq  27849  sltval  27922  nocvxminlem  27965  nofulllem1  27977  elfuns  28080  brimg  28102  brsuccf  28106  dfrdg4  28115  tfrqfree  28116  brofs  28170  funtransport  28196  fvtransport  28197  brifs  28208  lineext  28241  brfs  28244  btwnconn1lem11  28262  btwnconn1lem14  28265  brsegle  28273  segletr  28279  segleantisym  28280  seglelin  28281  funray  28305  fvray  28306  funline  28307  fvline  28309  ellines  28317  linethru  28318  ptrest  28563  mblfinlem3  28568  mblfinlem4  28569  ismblfin  28570  mbfresfi  28576  itg2addnclem  28581  itg2addnclem3  28583  itg2addnc  28584  ftc1anclem7  28611  ftc1anc  28613  areacirclem5  28626  trer  28649  opnrebl2  28654  nn0prpwlem  28655  isfne4  28679  isfne2  28681  isfne3  28682  islocfin  28706  unirep  28744  fnopabeqd  28751  fdc  28779  fdc1  28780  istotbnd  28806  heibor1lem  28846  heibor  28858  isriscg  28928  iscringd  28937  isidlc  28953  prtlem16  29152  prtlem15  29158  ismrcd1  29172  ismrcd2  29173  mzpcompact2lem  29226  eldioph  29234  eldioph2  29238  eldioph2b  29239  eldioph3  29242  diophin  29249  diophun  29250  diophrex  29252  rexrabdioph  29270  fphpd  29293  fphpdo  29294  pellexlem3  29310  monotuz  29420  monotoddzzfi  29421  monotoddzz  29422  oddcomabszz  29423  jm2.27  29495  rmydioph  29501  expdiophlem1  29508  expdiophlem2  29509  aomclem6  29550  aomclem8  29552  islssfg  29561  islssfg2  29562  hbtlem2  29618  hbtlem4  29620  hbtlem5  29622  hbtlem6  29623  dgraaval  29639  flcidc  29669  2sbc6g  29807  2sbc5g  29808  iotasbc2  29812  pm14.122a  29814  pm14.123a  29817  fmul01  29899  fmuldfeqlem1  29901  fmuldfeq  29902  fmul01lt1lem1  29903  fmul01lt1lem2  29904  climmulf  29915  climexp  29916  climsuse  29919  climrecf  29920  climinff  29922  stoweidlem3  29936  stoweidlem4  29937  stoweidlem7  29940  stoweidlem15  29948  stoweidlem16  29949  stoweidlem17  29950  stoweidlem19  29952  stoweidlem20  29953  stoweidlem22  29955  stoweidlem23  29956  stoweidlem27  29960  stoweidlem30  29963  stoweidlem32  29965  stoweidlem34  29967  stoweidlem42  29975  stoweidlem43  29976  stoweidlem48  29981  stoweidlem51  29984  stoweidlem59  29992  stoweidlem60  29993  2reu4a  30151  f12dfv  30284  f13dfv  30285  oprabv  30295  usgra2wlkspthlem1  30434  wwlk  30453  wlklniswwlkn2  30472  el2wlkonot  30526  el2spthonot  30527  el2spthonot0  30528  usg2spthonot  30545  usg2spthonot0  30546  usg2spthonot1  30547  clwlkisclwwlklem0  30588  clwlkisclwwlk  30589  erclwwlktr0  30617  eleclclwwlkn  30645  usghashecclwwlk  30647  isrusgra  30682  rusgranumwlkl1  30697  1vwmgra  30733  3vfriswmgra  30735  3cyclfrgrarn1  30742  4cycl2vnunb  30747  vdn1frgrav2  30756  vdgn1frgrav2  30757  frgrancvvdeqlemB  30769  usg2spot2nb  30796  usgreg2spot  30798  2spotmdisj  30799  usgreghash2spot  30800  extwwlkfab  30821  numclwwlk2lem1  30833  numclwwlk5  30843  opeliun2xp  30858  mpt2mptx2  30862  telescfzgsum  30951  coe1fzgsumd  30980  lcoval  31053  lco0  31068  islinindfis  31090  snlindsntor  31112  mnd1  31128  bnj976  32071  bnj852  32214  bnj1014  32253  bnj1015  32254  bnj1118  32275  bnj1123  32277  bnj1148  32287  bnj1171  32291  bnj1373  32321  bnj1489  32347  bj-eleq2w  32658  bj-finsumval0  32889  fsumshftd  32908  fsumshftdOLD  32909  lsmsat  32959  lsmsatcv  32961  islshpat  32968  lcvfbr  32971  lcvbr  32972  lsatcv0  32982  islshpkrN  33071  cvrval  33220  cvrval2  33225  cvrnbtwn2  33226  cvlexch1  33279  hlsuprexch  33331  cvrval5  33365  cvrat  33372  cvrat42  33394  3dim0  33407  3dim2  33418  islpln3  33483  islpln5  33485  islvol3  33526  islvol5  33529  4atlem11  33559  lineset  33688  isline  33689  ispsubsp2  33696  isline2  33724  isline3  33726  elpaddat  33754  elpadd2at  33756  dalawlem15  33835  pclfinclN  33900  4atex  34026  4atex2  34027  4atex3  34031  ltrnu  34071  cdleme0nex  34240  cdleme31so  34329  cdleme31fv  34340  cdleme31fv2  34343  cdlemefrs29pre00  34345  cdlemefrs29cpre1  34348  cdlemftr3  34515  cdlemb3  34556  cdlemg6d  34571  cdlemg33b  34657  cdlemg33c  34658  cdlemg33e  34660  cdlemk42  34891  dvhopellsm  35068  dibelval3  35098  diblsmopel  35122  diclspsn  35145  dihval  35183  dihopelvalcpre  35199  dih1dimatlem  35280  dihglb2  35293  dochkrshp3  35339  dihjatcclem4  35372  dihjat1lem  35379  mapdval  35579  mapdpglem30  35653
  Copyright terms: Public domain W3C validator