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  2368  eleq2  2499  ceqsex2  3005  ceqsex6v  3009  vtocl2gaf  3032  vtocl4ga  3037  ceqsrex2v  3090  moeq3  3131  mob2  3134  eqreu  3146  nelrdva  3163  undif4  3730  r19.27z  3773  r19.27zv  3774  ssunsn2  4027  preq12bg  4046  prel12g  4047  opeq2  4055  ralunsn  4074  intab  4153  disjxun  4285  opabbid  4349  opthg  4562  pocl  4643  isso2i  4668  ordelord  4736  ordtri4  4751  xpeq2  4850  rabxp  4870  vtoclr  4878  opeliunxp  4885  posn  4902  opbrop  4911  elrnmpt1  5083  dfres2  5153  brcodir  5212  poltletr  5228  xp11  5268  fununi  5479  fneq2  5495  fnun  5512  feq3  5539  foeq3  5613  funbrfv  5725  ssimaexg  5752  fvopab3g  5765  fvopab3ig  5766  fvelrn  5834  fvcofneq  5846  fmptco  5871  elunirn  5963  isoeq2  6006  isoeq3  6007  isoini  6024  isopolem  6031  f1oiso  6037  f1oiso2  6038  oprabbid  6134  cbvoprab3  6157  mpt2mptx  6176  mpt2fun  6187  elrnmpt2res  6199  ov  6205  ov3  6222  ov6g  6223  ovg  6224  caoftrn  6350  dfwe2  6388  dflim4  6454  tfisi  6464  elxp4  6517  elxp5  6518  f1o2ndf1  6675  frxp  6677  xporderlem  6678  fnwelem  6682  brtpos2  6746  dftpos4  6759  onfununi  6794  recseq  6825  omopth  7089  brecop  7185  eroveu  7187  erovlem  7188  erov  7189  ecopovtrn  7195  th3qlem1  7198  th3qlem2  7199  th3q  7201  elpmg  7220  ixpsnval  7258  ixpsnf1o  7295  domeng  7316  dom2lem  7341  xpcomco  7393  xpassen  7397  xpdom2  7398  omxpenlem  7404  xpf1o  7465  unxpdom  7512  isinf  7518  findcard2  7544  findcard2d  7546  fiint  7580  supeq2  7690  wemapso2lem  7759  inf0  7819  cantnfp1lem3  7880  cantnfp1  7881  scott0  8085  isinffi  8154  isacn  8206  aceq1  8279  aceq0  8280  aceq2  8281  dfac3  8283  dfac5lem1  8285  dfac2  8292  dfac12lem2  8305  kmlem8  8318  kmlem14  8324  infmap2  8379  cfval  8408  cflim3  8423  sornom  8438  infpssrlem4  8467  isf32lem9  8522  domtriomlem  8603  axdc2lem  8609  zfac  8621  ac6num  8640  axrepndlem1  8748  axunndlem1  8751  axregnd  8762  axregndOLD  8763  axinfndlem1  8764  axacndlem4  8769  axacndlem5  8770  zfcndac  8778  fpwwe2lem5  8793  pwfseqlem4a  8820  pwfseqlem4  8821  alephgch  8833  wunex2  8897  tskord  8939  nqereu  9090  ordpipq  9103  prcdnq  9154  prnmax  9156  genpnnp  9166  distrlem5pr  9188  ltprord  9191  ltexprlem3  9199  ltexprlem4  9200  ltexpri  9204  prlem936  9208  reclem2pr  9209  ltsosr  9253  mulgt0sr  9264  ltresr  9299  axpre-lttrn  9325  axpre-mulgt0  9327  eqlelt  9454  lesub0  9848  wloglei  9864  mulle0b  10192  sup3  10279  infm3  10281  prime  10714  fzind  10732  uzwo  10909  uzwoOLD  10910  zbtwnre  10943  xltnegi  11178  xmulneg1  11224  ixxval  11300  fzval  11431  elfzm11  11520  elfzo  11547  seqof2  11856  nn0opth2  12042  facwordi  12057  hashnn0n0nn  12145  brfi1uzind  12211  wrdeqswrdlsw  12335  2swrd1eqwrdeq  12340  wrd2ind  12364  2swrd2eqwrdeq  12545  shftfval  12551  shftfib  12553  shftfn  12554  2shfti  12561  abs1m  12815  cau3lem  12834  caubnd2  12837  clim  12964  rlim  12965  clim2  12974  climi  12980  o1lo1  13007  rlimcn2  13060  climcn2  13062  addcn2  13063  subcn2  13064  mulcn2  13065  o1of2  13082  isercoll  13137  caurcvg2  13147  sumeq2w  13161  sumeq2ii  13162  summo  13186  fsum  13189  sinbnd  13456  cosbnd  13457  divalgb  13600  ndvdssub  13603  smupp1  13668  smueqlem  13678  gcdval  13684  gcdcllem2  13688  gcdneg  13702  gcdass  13721  algcvgblem  13744  prmind2  13766  qredeq  13784  euclemma  13786  qnumval  13807  qdenval  13808  eulerthlem2  13849  pceu  13905  pczpre  13906  pcdiv  13911  prmpwdvds  13957  prmreclem5  13973  vdwapun  14027  ramub2  14067  rami  14068  ramcl  14082  ismred2  14533  isacs  14581  iscatd2  14611  catpropd  14640  oppccatid  14650  isinv  14690  isssc  14725  funcres2b  14799  funcpropd  14802  fucinv  14875  yoniso  15087  prslem  15093  drsdir  15097  drsdirfi  15100  posi  15112  isposd  15117  pltval  15122  plttr  15132  isipodrs  15323  ipodrsima  15327  dirge  15399  mndlem1  15411  mrcmndind  15485  gsumpropd  15495  gsumress  15498  divsgrp2  15664  resscntz  15840  psgnunilem3  15993  psgneu  16003  psgnvali  16005  psgnvalii  16006  isslw  16098  subgslw  16106  iscmnd  16280  gsumval3eu  16372  gsumval3OLD  16373  gsumval3lem2  16375  dmdprd  16470  subgdmdprd  16521  dprd2d2  16533  pgpfac1  16571  pgpfaclem2  16573  pgpfaclem3  16574  pgpfac  16575  ablfaclem1  16576  divsrng2  16702  dvdsrval  16727  crngunit  16744  dfrhm2  16798  isdrngd  16837  abvpropd  16907  islmod  16932  lssacs  17028  lsspropd  17078  islmhm  17088  lbspropd  17160  ixpsnbasval  17270  fiidomfld  17360  ltbval  17533  opsrval  17536  mpfind  17602  pf1ind  17769  evl1gsumd  17771  psgndiflemA  18011  pjfval2  18114  frlmup1  18206  mdetralt  18394  mdetralt2  18395  mdetunilem1  18398  mdetunilem2  18399  mdetunilem9  18406  gsummatr01  18445  eltopspOLD  18503  istpsOLD  18505  basis2  18536  eltg2  18543  isclo  18671  isnei  18687  isneip  18689  neiptopnei  18716  restbas  18742  restcld  18756  neitr  18764  iscnp  18821  iscnp3  18828  tgcn  18836  cnpimaex  18840  lmbrf  18844  cncnp  18864  cnprest2  18874  isreg  18916  regsep  18918  isnrm  18919  ist1-2  18931  nrmsep3  18939  isnrm2  18942  hauscmplem  18989  dfcon2  19003  is1stc  19025  1stcclb  19028  1stcfb  19029  is2ndc  19030  2ndc1stc  19035  1stcrest  19037  2ndcsep  19043  1stccnp  19046  islly  19052  llyeq  19054  llyi  19058  hausllycmp  19078  lly1stc  19080  txbas  19120  ptpjpre1  19124  elpt  19125  txcnpi  19161  ptpjopn  19165  ptcldmpt  19167  ptclsg  19168  txcnp  19173  ptcnp  19175  hausdiag  19198  tx1stc  19203  xkoinjcn  19240  imasnopn  19243  imasncld  19244  imasncls  19245  fbfinnfr  19394  snfil  19417  uffix2  19477  elfm  19500  elfm2  19501  fmco  19514  hauspwpwf1  19540  flfnei  19544  isflf  19546  lmflf  19558  fclscf  19578  isfcf  19587  alexsublem  19596  cnextcn  19619  cnextfres  19620  eltsms  19683  tsmsresOLD  19697  tsmsres  19698  tsmsf1o  19699  ustuqtop4  19799  ispsmet  19860  ismet  19878  isxmet  19879  ismet2  19888  imasdsf1olem  19928  blres  19986  met2ndc  20078  metcnp3  20095  nrmmetd  20147  pi1grplem  20601  lmmbr2  20750  lmmbrf  20753  iscau2  20768  iscau4  20770  caucfil  20774  lmclim  20793  cfilucfil3OLD  20809  cfilucfil3  20810  bcthlem1  20815  bcth  20820  ishl2  20862  pmltpclem1  20912  elovolm  20938  ovolgelb  20943  ovolicc  20986  mbfaddlem  21118  i1fres  21163  mbfi1fseqlem4  21176  itg2l  21187  itg2leub  21192  itg2seq  21200  isibl  21223  iblitg  21226  dfitg  21227  itgeq2  21235  itgvallem  21242  iblcnlem1  21245  iblrelem  21248  iblpos  21250  ellimc3  21334  limciun  21349  limcun  21350  dvmptfsum  21427  dveflem  21431  lhop1lem  21465  dvfsumlem2  21479  dvfsumlem4  21481  mdegleb  21515  elply2  21644  plypf1  21660  coeval  21671  plydivlem4  21742  sincosq3sgn  21942  vmasum  22535  lgsqrlem1  22660  lgsquadlem1  22673  2sqlem8  22691  2sqlem9  22692  2sqlem11  22694  dchrisumlema  22717  dchrisumlem2  22719  pntibndlem3  22821  pntibnd  22822  pntleme  22837  pntlemp  22839  axtgsegcon  22905  axtg5seg  22906  axtgpasch  22908  iscgrg  22945  legov  22996  mirreu3  23038  brcgr  23114  brbtwn2  23119  colinearalg  23124  ax5seg  23152  axcontlem5  23182  axcontlem10  23187  usgraedg4  23273  cusgrafilem2  23356  cusgrafi  23358  uvtx01vtx  23368  usgrnloop  23430  spthonepeq  23454  usgrcyclnl2  23495  4cycl4v4e  23520  4cycl4dv4e  23522  iseupa  23554  eupath2lem3  23568  isgrpo  23651  isgrp2d  23690  isgrpda  23752  ismndo  23798  drngoi  23862  vci  23894  isvclem  23923  nmoofval  24130  nmooval  24131  nmosetn0  24133  nmoolb  24139  nmoubi  24140  nmoo0  24159  nmlno0lem  24161  isphg  24185  norm3lemt  24522  chlimi  24605  ocsh  24654  cmbr  24955  chscllem2  25009  spansncv  25024  eigorth  25210  nmopval  25228  nmopsetn0  25237  nmfnval  25248  nmfnsetn0  25250  nmoplb  25279  nmfnlb  25296  nmopnegi  25337  nmop0  25358  nmfn0  25359  nmlnop0iALT  25367  nmopun  25386  nmcexi  25398  branmfn  25477  leopmuli  25505  pjnmopi  25520  cvbr  25654  mdbr  25666  dmdbr  25671  atom1d  25725  chrelat2  25742  atcvati  25758  atord  25760  atcvat2  25761  chirredlem4  25765  mdsymlem5  25779  disjunsn  25904  fmptcof2  25947  ofpreima  25952  funcnv4mpt  25957  mpt2mptxf  25963  2ndpreima  25970  f1od2  25992  xeqlelt  26034  ishashinf  26053  ressprs  26084  isomnd  26132  archiabllem2a  26179  archiabl  26183  isslmd  26186  gsumle  26214  gsumvsca1  26219  gsumvsca2  26220  esumcvg  26504  sitgval  26687  eulerpartlemmf  26727  eulerpartlemgvv  26728  eulerpartlemn  26733  eulerpart  26734  brafs  26965  lgamgulmlem2  26985  erdszelem3  27050  erdsze  27059  pconcn  27082  cnpcon  27088  txpcon  27090  conpcon  27093  cvmscbv  27116  iscvm  27117  cvmsi  27123  cvmsval  27124  relexp0  27300  relexpsucr  27301  relexpsucl  27303  relexpadd  27309  relexpindlem  27310  prodfdiv  27380  ntrivcvgn0  27382  ntrivcvgmullem  27385  prodeq1f  27390  prodeq2w  27394  prodeq2ii  27395  prodmo  27418  zprod  27419  fprod  27423  fprodntriv  27424  elima4  27559  dfrdg2  27578  dfrdg3  27579  elpred  27607  trpredrec  27671  poseq  27683  soseq  27684  sltval  27757  nocvxminlem  27800  nofulllem1  27812  elfuns  27915  brimg  27937  brsuccf  27941  dfrdg4  27950  tfrqfree  27951  brofs  28005  funtransport  28031  fvtransport  28032  brifs  28043  lineext  28076  brfs  28079  btwnconn1lem11  28097  btwnconn1lem14  28100  brsegle  28108  segletr  28114  segleantisym  28115  seglelin  28116  funray  28140  fvray  28141  funline  28142  fvline  28144  ellines  28152  linethru  28153  ptrest  28396  mblfinlem3  28401  mblfinlem4  28402  ismblfin  28403  mbfresfi  28409  itg2addnclem  28414  itg2addnclem3  28416  itg2addnc  28417  ftc1anclem7  28444  ftc1anc  28446  areacirclem5  28459  trer  28482  opnrebl2  28487  nn0prpwlem  28488  isfne4  28512  isfne2  28514  isfne3  28515  islocfin  28539  unirep  28577  fnopabeqd  28584  fdc  28612  fdc1  28613  istotbnd  28639  heibor1lem  28679  heibor  28691  isriscg  28761  iscringd  28770  isidlc  28786  prtlem16  28985  prtlem15  28991  ismrcd1  29005  ismrcd2  29006  mzpcompact2lem  29059  eldioph  29067  eldioph2  29071  eldioph2b  29072  eldioph3  29075  diophin  29082  diophun  29083  diophrex  29085  rexrabdioph  29103  fphpd  29126  fphpdo  29127  pellexlem3  29143  monotuz  29253  monotoddzzfi  29254  monotoddzz  29255  oddcomabszz  29256  jm2.27  29328  rmydioph  29334  expdiophlem1  29341  expdiophlem2  29342  aomclem6  29383  aomclem8  29385  islssfg  29394  islssfg2  29395  hbtlem2  29451  hbtlem4  29453  hbtlem5  29455  hbtlem6  29456  dgraaval  29472  flcidc  29502  2sbc6g  29640  2sbc5g  29641  iotasbc2  29645  pm14.122a  29647  pm14.123a  29650  fmul01  29732  fmuldfeqlem1  29734  fmuldfeq  29735  fmul01lt1lem1  29736  fmul01lt1lem2  29737  climmulf  29748  climexp  29749  climsuse  29752  climrecf  29753  climinff  29755  stoweidlem3  29769  stoweidlem4  29770  stoweidlem7  29773  stoweidlem15  29781  stoweidlem16  29782  stoweidlem17  29783  stoweidlem19  29785  stoweidlem20  29786  stoweidlem22  29788  stoweidlem23  29789  stoweidlem27  29793  stoweidlem30  29796  stoweidlem32  29798  stoweidlem34  29800  stoweidlem42  29808  stoweidlem43  29809  stoweidlem48  29814  stoweidlem51  29817  stoweidlem59  29825  stoweidlem60  29826  2reu4a  29984  f12dfv  30117  f13dfv  30118  oprabv  30128  usgra2wlkspthlem1  30267  wwlk  30286  wlklniswwlkn2  30305  el2wlkonot  30359  el2spthonot  30360  el2spthonot0  30361  usg2spthonot  30378  usg2spthonot0  30379  usg2spthonot1  30380  clwlkisclwwlklem0  30421  clwlkisclwwlk  30422  erclwwlktr0  30450  eleclclwwlkn  30478  usghashecclwwlk  30480  isrusgra  30515  rusgranumwlkl1  30530  1vwmgra  30566  3vfriswmgra  30568  3cyclfrgrarn1  30575  4cycl2vnunb  30580  vdn1frgrav2  30589  vdgn1frgrav2  30590  frgrancvvdeqlemB  30602  usg2spot2nb  30629  usgreg2spot  30631  2spotmdisj  30632  usgreghash2spot  30633  extwwlkfab  30654  numclwwlk2lem1  30666  numclwwlk5  30676  opeliun2xp  30690  mpt2mptx2  30694  coe1fzgsumd  30803  lcoval  30877  lco0  30892  islinindfis  30914  snlindsntor  30936  mnd1  30952  bnj976  31700  bnj852  31843  bnj1014  31882  bnj1015  31883  bnj1118  31904  bnj1123  31906  bnj1148  31916  bnj1171  31920  bnj1373  31950  bnj1489  31976  bj-eleq2w  32258  bj-finsumval0  32479  lsmsat  32546  lsmsatcv  32548  islshpat  32555  lcvfbr  32558  lcvbr  32559  lsatcv0  32569  islshpkrN  32658  cvrval  32807  cvrval2  32812  cvrnbtwn2  32813  cvlexch1  32866  hlsuprexch  32918  cvrval5  32952  cvrat  32959  cvrat42  32981  3dim0  32994  3dim2  33005  islpln3  33070  islpln5  33072  islvol3  33113  islvol5  33116  4atlem11  33146  lineset  33275  isline  33276  ispsubsp2  33283  isline2  33311  isline3  33313  elpaddat  33341  elpadd2at  33343  dalawlem15  33422  pclfinclN  33487  4atex  33613  4atex2  33614  4atex3  33618  ltrnu  33658  cdleme0nex  33827  cdleme31so  33916  cdleme31fv  33927  cdleme31fv2  33930  cdlemefrs29pre00  33932  cdlemefrs29cpre1  33935  cdlemftr3  34102  cdlemb3  34143  cdlemg6d  34158  cdlemg33b  34244  cdlemg33c  34245  cdlemg33e  34247  cdlemk42  34478  dvhopellsm  34655  dibelval3  34685  diblsmopel  34709  diclspsn  34732  dihval  34770  dihopelvalcpre  34786  dih1dimatlem  34867  dihglb2  34880  dochkrshp3  34926  dihjatcclem4  34959  dihjat1lem  34966  mapdval  35166  mapdpglem30  35240
  Copyright terms: Public domain W3C validator