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

Theorem anbi2d 708
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 26 . 2  |-  ( ph  ->  ( th  ->  ( ps 
<->  ch ) ) )
32pm5.32d 643 1  |-  ( ph  ->  ( ( th  /\  ps )  <->  ( th  /\  ch ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  anbi2  712  anbi12d  715  bi2anan9  881  eleq2dALT  2487  ceqsex2  3055  ceqsex6v  3059  vtocl2gaf  3082  vtocl4ga  3087  ceqsrex2v  3142  moeq3  3183  mob2  3186  eqreu  3198  reu2eqd  3203  nelrdva  3217  undif4  3787  r19.27z  3834  r19.27zv  3835  ssunsn2  4095  preq12bg  4115  prel12g  4116  opeq2  4124  ralunsn  4143  intab  4222  disjxun  4357  opabbid  4422  opthg  4632  pocl  4717  isso2i  4742  xpeq2  4804  rabxp  4826  vtoclr  4834  opeliunxp  4841  posn  4858  opbrop  4869  elrnmpt1  5038  dfres2  5112  brcodir  5174  poltletr  5187  xp11  5227  elpred  5348  ordelord  5400  ordtri4  5415  fununi  5603  fneq2  5619  fnun  5636  feq3  5666  foeq3  5744  funbrfv  5856  ssimaexg  5884  fvopab3g  5897  fvopab3ig  5898  fvelrn  5967  fvcofneq  5982  fmptco  6008  elunirn  6108  f12dfv  6124  f13dfv  6125  isoeq2  6163  isoeq3  6164  isoini  6181  isopolem  6188  f1oiso  6194  f1oiso2  6195  riotabidv  6206  oprabv  6290  oprabbid  6295  cbvoprab3  6318  mpt2mptx  6338  mpt2fun  6349  elrnmpt2res  6361  ov  6367  ov3  6384  ov6g  6385  ovg  6386  caoftrn  6517  dfwe2  6559  dflim4  6626  tfisi  6636  elxp4  6688  elxp5  6689  f1o2ndf1  6852  frxp  6854  xporderlem  6855  fnwelem  6859  brtpos2  6927  dftpos4  6940  onfununi  7008  omopth  7307  brecop  7404  eroveu  7406  erovlem  7407  erov  7408  ecopovtrn  7414  elpmg  7435  ixpsnval  7473  ixpsnf1o  7510  domeng  7531  dom2lem  7556  xpcomco  7608  xpassen  7612  xpdom2  7613  omxpenlem  7619  xpf1o  7680  unxpdom  7725  isinf  7731  findcard2  7757  findcard2d  7759  fiint  7794  supeq2  7908  wemapso2lem  8013  inf0  8072  cantnfp1lem3  8130  cantnfp1  8131  scott0  8302  isinffi  8371  isacn  8419  aceq1  8492  aceq0  8493  aceq2  8494  dfac3  8496  dfac5lem1  8498  dfac2  8505  dfac12lem2  8518  kmlem8  8531  kmlem14  8537  infmap2  8592  cfval  8621  cflim3  8636  sornom  8651  infpssrlem4  8680  isf32lem9  8735  domtriomlem  8816  axdc2lem  8822  zfac  8834  ac6num  8853  axrepndlem1  8961  axunndlem1  8964  axregnd  8973  axinfndlem1  8974  axacndlem4  8979  axacndlem5  8980  zfcndac  8988  fpwwe2lem5  9003  pwfseqlem4a  9030  pwfseqlem4  9031  alephgch  9043  wunex2  9107  tskord  9149  nqereu  9298  ordpipq  9311  prcdnq  9362  prnmax  9364  genpnnp  9374  distrlem5pr  9396  ltprord  9399  ltexprlem3  9407  ltexprlem4  9408  ltexpri  9412  prlem936  9416  reclem2pr  9417  addsrmo  9441  mulsrmo  9442  addsrpr  9443  mulsrpr  9444  ltsosr  9462  mulgt0sr  9473  ltresr  9508  axpre-lttrn  9534  axpre-mulgt0  9536  eqlelt  9665  lesub0  10075  wloglei  10090  mulle0b  10420  sup3  10510  infm3  10512  prime  10960  fzind  10977  uzwo  11166  zbtwnre  11206  xltnegi  11453  xmulneg1  11499  ixxval  11587  fzval  11730  elfzm11  11809  elfzo  11866  seqof2  12214  nn0opth2  12401  facwordi  12417  hashnn0n0nn  12513  ishashinf  12567  fi1uzind  12591  brfi1indALT  12594  2swrd1eqwrdeq  12749  wrd2ind  12773  cshwcsh2id  12866  2swrd2eqwrdeq  12965  relexpsucnnr  13025  relexprelg  13038  relexpindlem  13063  shftfval  13070  shftfib  13072  shftfn  13073  2shfti  13080  abs1m  13335  cau3lem  13354  caubnd2  13357  clim  13494  rlim  13495  clim2  13504  climi  13510  o1lo1  13537  rlimcn2  13590  climcn2  13592  addcn2  13593  subcn2  13594  mulcn2  13595  o1of2  13612  isercoll  13667  caurcvg2  13680  sumeq2w  13694  sumeq2ii  13695  summo  13719  fsum  13722  prodfdiv  13888  ntrivcvgn0  13890  ntrivcvgmullem  13893  prodeq1f  13898  prodeq2w  13902  prodeq2ii  13903  prodmo  13926  zprod  13927  fprod  13931  fprodntriv  13932  fproddivf  13977  fprodsplitf  13978  fprodsplit1f  13980  sinbnd  14170  cosbnd  14171  divalgb  14321  ndvdssub  14324  smupp1  14390  smueqlem  14400  gcdval  14406  gcdcllem2  14410  gcdneg  14426  gcdass  14449  algcvgblem  14472  lcmval  14491  lcmvalOLD  14492  lcmneg  14504  lcmgcdlem  14507  lcmass  14515  prmind2  14571  qredeq  14599  euclemma  14601  qnumval  14622  qdenval  14623  eulerthlem2  14666  pceu  14732  pczpre  14733  pcdiv  14738  prmpwdvds  14784  prmreclem5  14800  vdwapun  14860  ramub2  14907  rami  14908  ramcl  14923  ismred2  15445  isacs  15493  iscatd2  15523  catpropd  15550  oppccatid  15560  isinv  15601  isssc  15661  funcres2b  15738  funcpropd  15741  fucinv  15814  yoniso  16106  prslem  16112  drsdir  16116  drsdirfi  16119  posi  16131  isposd  16137  pltval  16142  plttr  16152  isipodrs  16343  ipodrsima  16347  dirge  16419  gsumpropd  16451  gsumress  16455  mnd1OLD  16514  mrcmndind  16549  mgmnsgrpex  16601  qusgrp2  16740  resscntz  16921  psgnunilem3  17073  psgneu  17083  psgnvali  17085  psgnvalii  17086  isslw  17196  subgslw  17204  iscmnd  17378  gsumval3eu  17474  gsumval3lem2  17476  telgsumfzs  17555  dmdprd  17566  subgdmdprd  17603  dprd2d2  17613  pgpfac1  17649  pgpfaclem2  17651  pgpfaclem3  17652  pgpfac  17653  ablfaclem1  17654  qusring2  17784  dvdsrval  17809  crngunit  17826  dfrhm2  17881  isdrngd  17936  abvpropd  18006  islmod  18031  lssacs  18126  lsspropd  18176  islmhm  18186  lbspropd  18258  ixpsnbasval  18368  fiidomfld  18468  ltbval  18631  opsrval  18634  mpfind  18695  coe1fzgsumd  18832  pf1ind  18879  evl1gsumd  18881  psgndiflemA  19104  pjfval2  19207  frlmup1  19291  scmatf1  19491  mdetralt  19568  mdetralt2  19569  mdetunilem1  19572  mdetunilem2  19573  mdetunilem9  19580  gsummatr01  19619  basis2  19901  eltg2  19908  isclo  20038  isnei  20054  isneip  20056  neiptopnei  20083  restbas  20109  restcld  20123  neitr  20131  iscnp  20188  iscnp3  20195  tgcn  20203  cnpimaex  20207  lmbrf  20211  cncnp  20231  cnprest2  20241  isreg  20283  regsep  20285  isnrm  20286  ist1-2  20298  nrmsep3  20306  isnrm2  20309  hauscmplem  20356  dfcon2  20369  is1stc  20391  1stcclb  20394  1stcfb  20395  is2ndc  20396  2ndc1stc  20401  1stcrest  20403  2ndcsep  20409  1stccnp  20412  islly  20418  llyeq  20420  llyi  20424  hausllycmp  20444  lly1stc  20446  islocfin  20467  txbas  20517  ptpjpre1  20521  elpt  20522  txcnpi  20558  ptpjopn  20562  ptcldmpt  20564  ptclsg  20565  txcnp  20570  ptcnp  20572  hausdiag  20595  tx1stc  20600  xkoinjcn  20637  imasnopn  20640  imasncld  20641  imasncls  20642  fbfinnfr  20791  snfil  20814  uffix2  20874  elfm  20897  elfm2  20898  fmco  20911  hauspwpwf1  20937  flfnei  20941  isflf  20943  lmflf  20955  fclscf  20975  isfcf  20984  alexsublem  20994  cnextcn  21017  cnextfres1  21018  eltsms  21082  tsmsres  21093  tsmsf1o  21094  ustuqtop4  21194  ispsmet  21255  ismet  21273  isxmet  21274  ismet2  21283  imasdsf1olem  21323  blres  21381  met2ndc  21473  metcnp3  21490  nrmmetd  21524  pi1grplem  22015  lmmbr2  22164  lmmbrf  22167  iscau2  22182  iscau4  22184  caucfil  22188  lmclim  22207  cfilucfil3  22223  bcthlem1  22227  bcth  22232  ishl2  22272  pmltpclem1  22334  elovolm  22363  ovolgelb  22368  ovolicc  22412  mbfaddlem  22551  i1fres  22598  mbfi1fseqlem4  22611  itg2l  22622  itg2leub  22627  itg2seq  22635  isibl  22658  iblitg  22661  dfitg  22662  itgeq2  22670  itgvallem  22677  iblcnlem1  22680  iblrelem  22683  iblpos  22685  ellimc3  22769  limciun  22784  limcun  22785  dvmptfsum  22862  dveflem  22866  lhop1lem  22900  dvfsumlem2  22914  dvfsumlem4  22916  mdegleb  22948  elply2  23085  plypf1  23101  coeval  23112  plydivlem4  23184  sincosq3sgn  23390  lgamgulmlem2  23890  vmasum  24079  lgsqrlem1  24204  lgsquadlem1  24217  2sqlem8  24235  2sqlem9  24236  2sqlem11  24238  dchrisumlema  24261  dchrisumlem2  24263  pntibndlem3  24365  pntibnd  24366  pntleme  24381  pntlemp  24383  axtgsegcon  24447  axtg5seg  24448  axtgpasch  24450  iscgrg  24492  legov  24565  ltgov  24577  ishlg  24582  mirreu3  24634  israg  24677  islnopp  24716  ishpg  24736  iscgra  24786  isinag  24814  isleag  24818  brcgr  24865  brbtwn2  24870  colinearalg  24875  ax5seg  24903  axcontlem5  24933  axcontlem10  24938  usgraedg4  25049  cusgrafilem2  25143  cusgrafi  25145  uvtx01vtx  25155  usgrwlknloop  25228  spthonepeq  25252  usgra2adedgwlkonALT  25279  usgra2wlkspthlem1  25282  usgrcyclnl2  25304  4cycl4v4e  25329  4cycl4dv4e  25331  wwlk  25344  wlklniswwlkn2  25363  clwlkisclwwlklem0  25451  clwlkisclwwlk  25452  eleclclwwlkn  25496  usghashecclwwlk  25498  el2wlkonot  25532  el2spthonot  25533  el2spthonot0  25534  usg2spthonot  25551  usg2spthonot0  25552  usg2spthonot1  25553  isrusgra  25590  isrusgusrg  25595  isrgrac  25597  isrusgrac  25598  rusgranumwlkl1  25610  iseupa  25628  eupath2lem3  25642  1vwmgra  25666  3vfriswmgra  25668  3cyclfrgrarn1  25675  4cycl2vnunb  25680  vdn1frgrav2  25688  vdgn1frgrav2  25689  frgrancvvdeqlemB  25701  usg2spot2nb  25728  usgreg2spot  25730  2spotmdisj  25731  usgreghash2spot  25732  extwwlkfab  25753  numclwwlk2lem1  25765  numclwwlk5  25775  isgrpo  25859  isgrp2d  25898  isgrpda  25960  ismndo  26006  drngoi  26070  vci  26102  isvclem  26131  nmoofval  26338  nmooval  26339  nmosetn0  26341  nmoolb  26347  nmoubi  26348  nmoo0  26367  nmlno0lem  26369  isphg  26393  norm3lemt  26740  chlimi  26822  ocsh  26871  cmbr  27172  chscllem2  27226  spansncv  27241  eigorth  27426  nmopval  27444  nmopsetn0  27453  nmfnval  27464  nmfnsetn0  27466  nmoplb  27495  nmfnlb  27512  nmopnegi  27553  nmop0  27574  nmfn0  27575  nmlnop0iALT  27583  nmopun  27602  nmcexi  27614  branmfn  27693  leopmuli  27721  pjnmopi  27736  cvbr  27870  mdbr  27882  dmdbr  27887  atom1d  27941  chrelat2  27958  atcvati  27974  atord  27976  atcvat2  27977  chirredlem4  27981  mdsymlem5  27995  disjunsn  28143  opeldifid  28149  fcoinvbr  28154  fimarab  28183  fmptcof2  28198  aciunf1lem  28203  ofpreima  28207  funcnv4mpt  28212  mpt2mptxf  28219  2ndpreima  28227  f1od2  28252  fpwrelmapffslem  28260  xeqlelt  28301  ressprs  28360  isomnd  28408  archiabllem2a  28455  archiabl  28459  isslmd  28462  gsumle  28486  gsumvsca1  28490  gsumvsca2  28491  orngmul  28511  smatrcl  28567  ismntop  28775  esumcvg  28852  fiunelros  28941  pmeasadd  29103  sitgval  29110  eulerpartlemmf  29153  eulerpartlemgvv  29154  eulerpartlemn  29159  eulerpart  29160  brafs  29434  bnj976  29534  bnj852  29677  bnj1014  29716  bnj1015  29717  bnj1118  29738  bnj1123  29740  bnj1148  29750  bnj1171  29754  bnj1373  29784  bnj1489  29810  erdszelem3  29861  erdsze  29870  pconcn  29892  cnpcon  29898  txpcon  29900  conpcon  29903  cvmscbv  29926  iscvm  29927  cvmsi  29933  cvmsval  29934  mclsval  30146  mclsppslem  30166  elima4  30365  dfrdg2  30386  dfrdg3  30387  trpredrec  30423  poseq  30435  soseq  30436  sltval  30478  nocvxminlem  30521  nofulllem1  30533  elfuns  30624  brimg  30646  dfrecs2  30659  dfrdg4  30660  brofs  30714  funtransport  30740  fvtransport  30741  brifs  30752  lineext  30785  brfs  30788  btwnconn1lem11  30806  btwnconn1lem14  30809  brsegle  30817  segletr  30823  segleantisym  30824  seglelin  30825  funray  30849  fvray  30850  funline  30851  fvline  30853  ellines  30861  linethru  30862  fwddifnp1  30874  trer  30914  opnrebl2  30919  nn0prpwlem  30920  isfne4  30938  isfne2  30940  isfne3  30941  bj-eleq2w  31363  bj-finsumval0  31603  mptsnunlem  31641  topdifinfindis  31650  icoreval  31657  isbasisrelowllem1  31659  isbasisrelowllem2  31660  relowlssretop  31667  relowlpssretop  31668  finxpeq1  31679  finxpreclem6  31689  finxpsuclem  31690  ptrest  31840  ptrecube  31841  poimirlem1  31842  poimirlem13  31854  poimirlem14  31855  poimirlem17  31858  poimirlem18  31859  poimirlem20  31861  poimirlem21  31862  poimirlem22  31863  poimirlem24  31865  poimirlem25  31866  poimirlem26  31867  poimirlem27  31868  poimirlem28  31869  poimirlem29  31870  poimirlem31  31872  poimirlem32  31873  poimir  31874  mblfinlem3  31880  mblfinlem4  31881  ismblfin  31882  mbfresfi  31888  itg2addnclem  31894  itg2addnclem3  31896  itg2addnc  31897  ftc1anclem7  31924  ftc1anc  31926  areacirclem5  31937  unirep  31940  fnopabeqd  31947  fdc  31975  fdc1  31976  istotbnd  32002  heibor1lem  32042  heibor  32054  isriscg  32124  iscringd  32133  isidlc  32149  prtlem16  32346  prtlem15  32352  fsumshftd  32429  fsumshftdOLD  32430  lsmsat  32480  lsmsatcv  32482  islshpat  32489  lcvfbr  32492  lcvbr  32493  lsatcv0  32503  islshpkrN  32592  cvrval  32741  cvrval2  32746  cvrnbtwn2  32747  cvlexch1  32800  hlsuprexch  32852  cvrval5  32886  cvrat  32893  cvrat42  32915  3dim0  32928  3dim2  32939  islpln3  33004  islpln5  33006  islvol3  33047  islvol5  33050  4atlem11  33080  lineset  33209  isline  33210  ispsubsp2  33217  isline2  33245  isline3  33247  elpaddat  33275  elpadd2at  33277  dalawlem15  33356  pclfinclN  33421  4atex  33547  4atex2  33548  4atex3  33552  ltrnu  33592  cdleme0nex  33762  cdleme31so  33852  cdleme31fv  33863  cdleme31fv2  33866  cdlemefrs29pre00  33868  cdlemefrs29cpre1  33871  cdlemftr3  34038  cdlemb3  34079  cdlemg6d  34094  cdlemg33b  34180  cdlemg33c  34181  cdlemg33e  34183  cdlemk42  34414  dvhopellsm  34591  dibelval3  34621  diblsmopel  34645  diclspsn  34668  dihval  34706  dihopelvalcpre  34722  dih1dimatlem  34803  dihglb2  34816  dochkrshp3  34862  dihjatcclem4  34895  dihjat1lem  34902  mapdval  35102  mapdpglem30  35176  ismrcd1  35446  ismrcd2  35447  mzpcompact2lem  35499  eldioph  35506  eldioph2  35510  eldioph2b  35511  eldioph3  35514  diophin  35521  diophun  35522  diophrex  35524  rexrabdioph  35543  fphpd  35565  fphpdo  35566  pellexlem3  35582  monotuz  35696  monotoddzzfi  35697  monotoddzz  35698  oddcomabszz  35699  jm2.27  35770  rmydioph  35776  expdiophlem1  35783  expdiophlem2  35784  aomclem6  35824  aomclem8  35826  islssfg  35835  islssfg2  35836  hbtlem2  35890  hbtlem4  35892  hbtlem5  35894  hbtlem6  35895  dgraaval  35912  dgraavalOLD  35913  flcidc  35947  ifpbi3  36018  dfhe3  36277  dvgrat  36568  cvgdvgrat  36569  binomcxplemnotnn0  36612  2sbc6g  36673  2sbc5g  36674  iotasbc2  36678  pm14.122a  36680  pm14.123a  36683  fiiuncl  37316  disjf1  37355  disjinfi  37366  monoords  37405  fperiodmullem  37412  supxrgere  37447  supxrgelem  37451  supxrge  37452  xrlexaddrp  37466  fsumclf  37523  fsumsplitf  37524  fsummulc1f  37525  fsumnncl  37528  fsumsplit1  37529  fsumf1of  37531  fsumreclf  37533  fsumlessf  37534  fmul01  37535  fmuldfeqlem1  37537  fmuldfeq  37538  fmul01lt1lem1  37539  fmul01lt1lem2  37540  fprodexp  37551  fprodabs2  37552  climmulf  37559  climexp  37560  climsuse  37564  climrecf  37565  climinff  37567  climinffOLD  37568  climaddf  37572  mullimc  37573  limcdm0  37575  climf  37579  mullimcf  37580  constlimc  37581  idlimc  37583  limcperiod  37585  sumnnodd  37587  clim2f  37593  limcleqr  37602  neglimc  37605  addlimc  37606  0ellimcdiv  37607  cncfshift  37628  cncfperiod  37633  icccncfext  37642  fprodcncf  37656  fperdvper  37667  ioodvbdlimc1lem2  37681  ioodvbdlimc1lem2OLD  37683  ioodvbdlimc2lem  37685  ioodvbdlimc2lemOLD  37686  dvmptmulf  37689  dvnmptdivc  37690  dvnmul  37695  dvmptfprod  37697  dvnprodlem1  37698  dvnprodlem2  37699  iblspltprt  37727  itgspltprt  37733  stoweidlem3  37740  stoweidlem4  37741  stoweidlem7  37744  stoweidlem15  37752  stoweidlem16  37753  stoweidlem17  37754  stoweidlem19  37756  stoweidlem20  37757  stoweidlem22  37759  stoweidlem23  37760  stoweidlem27  37764  stoweidlem30  37768  stoweidlem32  37770  stoweidlem34  37772  stoweidlem42  37780  stoweidlem43  37781  stoweidlem48  37786  stoweidlem51  37789  stoweidlem59  37797  stoweidlem60  37798  dirkercncflem2  37843  fourierdlem2  37848  fourierdlem3  37849  fourierdlem11  37857  fourierdlem12  37858  fourierdlem15  37861  fourierdlem16  37862  fourierdlem21  37867  fourierdlem34  37881  fourierdlem41  37888  fourierdlem42  37889  fourierdlem42OLD  37890  fourierdlem46  37893  fourierdlem48  37895  fourierdlem49  37896  fourierdlem50  37897  fourierdlem51  37898  fourierdlem54  37901  fourierdlem68  37915  fourierdlem71  37918  fourierdlem72  37919  fourierdlem73  37920  fourierdlem76  37923  fourierdlem79  37926  fourierdlem81  37928  fourierdlem83  37930  fourierdlem86  37933  fourierdlem87  37934  fourierdlem89  37936  fourierdlem90  37937  fourierdlem91  37938  fourierdlem92  37939  fourierdlem94  37941  fourierdlem97  37944  fourierdlem103  37950  fourierdlem104  37951  fourierdlem107  37954  fourierdlem111  37958  fourierdlem112  37959  fourierdlem113  37960  etransclem2  37978  etransclem46  38022  intsaluni  38046  sge0f1o  38069  sge0lempt  38097  sge0iunmptlemfi  38100  sge0p1  38101  sge0fodjrnlem  38103  sge0iunmpt  38105  sge0ltfirpmpt2  38113  sge0isummpt2  38119  sge0xaddlem2  38121  sge0xadd  38122  meadjiun  38149  isomenndlem  38196  ovnlecvr  38221  ovnpnfelsup  38222  ovn0lem  38228  ovnsubaddlem1  38233  hoidmvlelem2  38259  hoidmvlelem3  38260  hoidmvlelem4  38261  ovnhoilem1  38264  ovnhoi  38266  2reu4a  38418  iccpartgt  38548  isgboa  38661  nnsum3primes4  38690  nnsum3primesprm  38692  nnsum3primesgbe  38694  nnsum3primesle9  38696  bgoldbachlt  38713  tgoldbachlt  38716  pfxsuff1eqwrdeq  38755  opfusgr  39119  nbusgredgeu0  39172  cusgrfilem2  39239  cusgrfi  39241  isfusgracl  39323  rngcinv  39568  rngcinvALTV  39580  ringcinv  39619  ringcinvALTV  39643  opeliun2xp  39701  mpt2mptx2  39703  lcoval  39792  lco0  39807  islinindfis  39829  snlindsntor  39851  nnlog2ge0lt1  39964
  Copyright terms: Public domain W3C validator