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  2491  eleq2OLD  2495  ceqsex2  3116  ceqsex6v  3120  vtocl2gaf  3143  vtocl4ga  3148  ceqsrex2v  3204  moeq3  3245  mob2  3248  eqreu  3260  reu2eqd  3265  nelrdva  3278  undif4  3846  r19.27z  3893  r19.27zv  3894  ssunsn2  4153  preq12bg  4173  prel12g  4174  opeq2  4182  ralunsn  4201  intab  4280  disjxun  4415  opabbid  4479  opthg  4688  pocl  4773  isso2i  4798  xpeq2  4860  rabxp  4882  vtoclr  4890  opeliunxp  4897  posn  4914  opbrop  4925  elrnmpt1  5094  dfres2  5168  brcodir  5230  poltletr  5243  xp11  5283  elpred  5403  ordelord  5455  ordtri4  5470  fununi  5658  fneq2  5674  fnun  5691  feq3  5721  foeq3  5799  funbrfv  5910  ssimaexg  5938  fvopab3g  5951  fvopab3ig  5952  fvelrn  6021  fvcofneq  6036  fmptco  6062  elunirn  6162  f12dfv  6178  f13dfv  6179  isoeq2  6217  isoeq3  6218  isoini  6235  isopolem  6242  f1oiso  6248  f1oiso2  6249  riotabidv  6260  oprabv  6344  oprabbid  6349  cbvoprab3  6372  mpt2mptx  6392  mpt2fun  6403  elrnmpt2res  6415  ov  6421  ov3  6438  ov6g  6439  ovg  6440  caoftrn  6571  dfwe2  6613  dflim4  6680  tfisi  6690  elxp4  6742  elxp5  6743  f1o2ndf1  6906  frxp  6908  xporderlem  6909  fnwelem  6913  brtpos2  6978  dftpos4  6991  onfununi  7059  omopth  7358  brecop  7455  eroveu  7457  erovlem  7458  erov  7459  ecopovtrn  7465  elpmg  7486  ixpsnval  7524  ixpsnf1o  7561  domeng  7582  dom2lem  7607  xpcomco  7659  xpassen  7663  xpdom2  7664  omxpenlem  7670  xpf1o  7731  unxpdom  7776  isinf  7782  findcard2  7808  findcard2d  7810  fiint  7845  supeq2  7959  wemapso2lem  8058  inf0  8117  cantnfp1lem3  8175  cantnfp1  8176  scott0  8347  isinffi  8416  isacn  8464  aceq1  8537  aceq0  8538  aceq2  8539  dfac3  8541  dfac5lem1  8543  dfac2  8550  dfac12lem2  8563  kmlem8  8576  kmlem14  8582  infmap2  8637  cfval  8666  cflim3  8681  sornom  8696  infpssrlem4  8725  isf32lem9  8780  domtriomlem  8861  axdc2lem  8867  zfac  8879  ac6num  8898  axrepndlem1  9006  axunndlem1  9009  axregnd  9018  axinfndlem1  9019  axacndlem4  9024  axacndlem5  9025  zfcndac  9033  fpwwe2lem5  9048  pwfseqlem4a  9075  pwfseqlem4  9076  alephgch  9088  wunex2  9152  tskord  9194  nqereu  9343  ordpipq  9356  prcdnq  9407  prnmax  9409  genpnnp  9419  distrlem5pr  9441  ltprord  9444  ltexprlem3  9452  ltexprlem4  9453  ltexpri  9457  prlem936  9461  reclem2pr  9462  addsrmo  9486  mulsrmo  9487  addsrpr  9488  mulsrpr  9489  ltsosr  9507  mulgt0sr  9518  ltresr  9553  axpre-lttrn  9579  axpre-mulgt0  9581  eqlelt  9710  lesub0  10120  wloglei  10135  mulle0b  10465  sup3  10555  infm3  10557  prime  11005  fzind  11022  uzwo  11211  zbtwnre  11251  xltnegi  11498  xmulneg1  11544  ixxval  11632  fzval  11773  elfzm11  11852  elfzo  11909  seqof2  12257  nn0opth2  12444  facwordi  12460  hashnn0n0nn  12556  brfi1uzind  12630  2swrd1eqwrdeq  12784  wrd2ind  12808  cshwcsh2id  12901  2swrd2eqwrdeq  12996  relexpsucnnr  13056  relexprelg  13069  relexpindlem  13094  shftfval  13101  shftfib  13103  shftfn  13104  2shfti  13111  abs1m  13366  cau3lem  13385  caubnd2  13388  clim  13525  rlim  13526  clim2  13535  climi  13541  o1lo1  13568  rlimcn2  13621  climcn2  13623  addcn2  13624  subcn2  13625  mulcn2  13626  o1of2  13643  isercoll  13698  caurcvg2  13711  sumeq2w  13725  sumeq2ii  13726  summo  13750  fsum  13753  prodfdiv  13919  ntrivcvgn0  13921  ntrivcvgmullem  13924  prodeq1f  13929  prodeq2w  13933  prodeq2ii  13934  prodmo  13957  zprod  13958  fprod  13962  fprodntriv  13963  fproddivf  14008  fprodsplitf  14009  fprodsplit1f  14011  sinbnd  14201  cosbnd  14202  divalgb  14349  ndvdssub  14352  smupp1  14417  smueqlem  14427  gcdval  14433  gcdcllem2  14437  gcdneg  14453  gcdass  14473  algcvgblem  14496  lcmval  14515  lcmvalOLD  14516  lcmneg  14528  lcmgcdlem  14531  lcmass  14539  prmind2  14595  qredeq  14623  euclemma  14625  qnumval  14646  qdenval  14647  eulerthlem2  14688  pceu  14748  pczpre  14749  pcdiv  14754  prmpwdvds  14800  prmreclem5  14816  vdwapun  14876  ramub2  14923  rami  14924  ramcl  14939  ismred2  15453  isacs  15501  iscatd2  15531  catpropd  15558  oppccatid  15568  isinv  15609  isssc  15669  funcres2b  15746  funcpropd  15749  fucinv  15822  yoniso  16114  prslem  16120  drsdir  16124  drsdirfi  16127  posi  16139  isposd  16145  pltval  16150  plttr  16160  isipodrs  16351  ipodrsima  16355  dirge  16427  gsumpropd  16459  gsumress  16463  mnd1OLD  16522  mrcmndind  16557  mgmnsgrpex  16609  qusgrp2  16748  resscntz  16929  psgnunilem3  17081  psgneu  17091  psgnvali  17093  psgnvalii  17094  isslw  17188  subgslw  17196  iscmnd  17370  gsumval3eu  17466  gsumval3lem2  17468  telgsumfzs  17547  dmdprd  17558  subgdmdprd  17595  dprd2d2  17605  pgpfac1  17641  pgpfaclem2  17643  pgpfaclem3  17644  pgpfac  17645  ablfaclem1  17646  qusring2  17776  dvdsrval  17801  crngunit  17818  dfrhm2  17873  isdrngd  17928  abvpropd  17998  islmod  18023  lssacs  18118  lsspropd  18168  islmhm  18178  lbspropd  18250  ixpsnbasval  18360  fiidomfld  18460  ltbval  18623  opsrval  18626  mpfind  18687  coe1fzgsumd  18824  pf1ind  18871  evl1gsumd  18873  psgndiflemA  19093  pjfval2  19196  frlmup1  19280  scmatf1  19480  mdetralt  19557  mdetralt2  19558  mdetunilem1  19561  mdetunilem2  19562  mdetunilem9  19569  gsummatr01  19608  basis2  19890  eltg2  19897  isclo  20027  isnei  20043  isneip  20045  neiptopnei  20072  restbas  20098  restcld  20112  neitr  20120  iscnp  20177  iscnp3  20184  tgcn  20192  cnpimaex  20196  lmbrf  20200  cncnp  20220  cnprest2  20230  isreg  20272  regsep  20274  isnrm  20275  ist1-2  20287  nrmsep3  20295  isnrm2  20298  hauscmplem  20345  dfcon2  20358  is1stc  20380  1stcclb  20383  1stcfb  20384  is2ndc  20385  2ndc1stc  20390  1stcrest  20392  2ndcsep  20398  1stccnp  20401  islly  20407  llyeq  20409  llyi  20413  hausllycmp  20433  lly1stc  20435  islocfin  20456  txbas  20506  ptpjpre1  20510  elpt  20511  txcnpi  20547  ptpjopn  20551  ptcldmpt  20553  ptclsg  20554  txcnp  20559  ptcnp  20561  hausdiag  20584  tx1stc  20589  xkoinjcn  20626  imasnopn  20629  imasncld  20630  imasncls  20631  fbfinnfr  20780  snfil  20803  uffix2  20863  elfm  20886  elfm2  20887  fmco  20900  hauspwpwf1  20926  flfnei  20930  isflf  20932  lmflf  20944  fclscf  20964  isfcf  20973  alexsublem  20983  cnextcn  21006  cnextfres1  21007  eltsms  21071  tsmsres  21082  tsmsf1o  21083  ustuqtop4  21183  ispsmet  21244  ismet  21262  isxmet  21263  ismet2  21272  imasdsf1olem  21312  blres  21370  met2ndc  21462  metcnp3  21479  nrmmetd  21513  pi1grplem  21966  lmmbr2  22115  lmmbrf  22118  iscau2  22133  iscau4  22135  caucfil  22139  lmclim  22158  cfilucfil3  22174  bcthlem1  22178  bcth  22183  ishl2  22223  pmltpclem1  22273  elovolm  22302  ovolgelb  22307  ovolicc  22351  mbfaddlem  22490  i1fres  22537  mbfi1fseqlem4  22550  itg2l  22561  itg2leub  22566  itg2seq  22574  isibl  22597  iblitg  22600  dfitg  22601  itgeq2  22609  itgvallem  22616  iblcnlem1  22619  iblrelem  22622  iblpos  22624  ellimc3  22708  limciun  22723  limcun  22724  dvmptfsum  22801  dveflem  22805  lhop1lem  22839  dvfsumlem2  22853  dvfsumlem4  22855  mdegleb  22887  elply2  23015  plypf1  23031  coeval  23042  plydivlem4  23114  sincosq3sgn  23317  lgamgulmlem2  23817  vmasum  24004  lgsqrlem1  24129  lgsquadlem1  24142  2sqlem8  24160  2sqlem9  24161  2sqlem11  24163  dchrisumlema  24186  dchrisumlem2  24188  pntibndlem3  24290  pntibnd  24291  pntleme  24306  pntlemp  24308  axtgsegcon  24372  axtg5seg  24373  axtgpasch  24375  iscgrg  24417  legov  24487  ltgov  24499  ishlg  24504  mirreu3  24556  israg  24596  islnopp  24635  ishpg  24654  iscgra  24704  isinag  24729  brcgr  24773  brbtwn2  24778  colinearalg  24783  ax5seg  24811  axcontlem5  24841  axcontlem10  24846  usgraedg4  24957  cusgrafilem2  25050  cusgrafi  25052  uvtx01vtx  25062  usgrnloop  25135  spthonepeq  25159  usgra2adedgwlkonALT  25186  usgra2wlkspthlem1  25189  usgrcyclnl2  25211  4cycl4v4e  25236  4cycl4dv4e  25238  wwlk  25251  wlklniswwlkn2  25270  clwlkisclwwlklem0  25358  clwlkisclwwlk  25359  eleclclwwlkn  25403  usghashecclwwlk  25405  el2wlkonot  25439  el2spthonot  25440  el2spthonot0  25441  usg2spthonot  25458  usg2spthonot0  25459  usg2spthonot1  25460  isrusgra  25497  isrusgusrg  25502  isrgrac  25504  isrusgrac  25505  rusgranumwlkl1  25517  iseupa  25535  eupath2lem3  25549  1vwmgra  25573  3vfriswmgra  25575  3cyclfrgrarn1  25582  4cycl2vnunb  25587  vdn1frgrav2  25595  vdgn1frgrav2  25596  frgrancvvdeqlemB  25608  usg2spot2nb  25635  usgreg2spot  25637  2spotmdisj  25638  usgreghash2spot  25639  extwwlkfab  25660  numclwwlk2lem1  25672  numclwwlk5  25682  isgrpo  25766  isgrp2d  25805  isgrpda  25867  ismndo  25913  drngoi  25977  vci  26009  isvclem  26038  nmoofval  26245  nmooval  26246  nmosetn0  26248  nmoolb  26254  nmoubi  26255  nmoo0  26274  nmlno0lem  26276  isphg  26300  norm3lemt  26637  chlimi  26719  ocsh  26768  cmbr  27069  chscllem2  27123  spansncv  27138  eigorth  27323  nmopval  27341  nmopsetn0  27350  nmfnval  27361  nmfnsetn0  27363  nmoplb  27392  nmfnlb  27409  nmopnegi  27450  nmop0  27471  nmfn0  27472  nmlnop0iALT  27480  nmopun  27499  nmcexi  27511  branmfn  27590  leopmuli  27618  pjnmopi  27633  cvbr  27767  mdbr  27779  dmdbr  27784  atom1d  27838  chrelat2  27855  atcvati  27871  atord  27873  atcvat2  27874  chirredlem4  27878  mdsymlem5  27892  disjunsn  28040  opeldifid  28046  fcoinvbr  28051  fimarab  28081  fmptcof2  28096  aciunf1lem  28101  ofpreima  28105  funcnv4mpt  28110  mpt2mptxf  28117  2ndpreima  28125  f1od2  28149  fpwrelmapffslem  28157  xeqlelt  28191  ishashinf  28214  ressprs  28251  isomnd  28299  archiabllem2a  28346  archiabl  28350  isslmd  28353  gsumle  28377  gsumvsca1  28381  gsumvsca2  28382  orngmul  28402  smatrcl  28458  ismntop  28666  esumcvg  28743  fiunelros  28832  pmeasadd  28983  sitgval  28990  eulerpartlemmf  29031  eulerpartlemgvv  29032  eulerpartlemn  29037  eulerpart  29038  brafs  29274  bnj976  29374  bnj852  29517  bnj1014  29556  bnj1015  29557  bnj1118  29578  bnj1123  29580  bnj1148  29590  bnj1171  29594  bnj1373  29624  bnj1489  29650  erdszelem3  29701  erdsze  29710  pconcn  29732  cnpcon  29738  txpcon  29740  conpcon  29743  cvmscbv  29766  iscvm  29767  cvmsi  29773  cvmsval  29774  mclsval  29986  mclsppslem  30006  elima4  30205  dfrdg2  30226  dfrdg3  30227  trpredrec  30263  poseq  30275  soseq  30276  sltval  30318  nocvxminlem  30361  nofulllem1  30373  elfuns  30464  brimg  30486  dfrecs2  30499  dfrdg4  30500  brofs  30554  funtransport  30580  fvtransport  30581  brifs  30592  lineext  30625  brfs  30628  btwnconn1lem11  30646  btwnconn1lem14  30649  brsegle  30657  segletr  30663  segleantisym  30664  seglelin  30665  funray  30689  fvray  30690  funline  30691  fvline  30693  ellines  30701  linethru  30702  fwddifnp1  30714  trer  30754  opnrebl2  30759  nn0prpwlem  30760  isfne4  30778  isfne2  30780  isfne3  30781  bj-eleq2w  31204  bj-finsumval0  31444  mptsnunlem  31471  topdifinfindis  31480  icoreval  31487  isbasisrelowllem1  31489  isbasisrelowllem2  31490  relowlssretop  31497  relowlpssretop  31498  ptrest  31643  ptrecube  31644  poimirlem1  31645  poimirlem13  31657  poimirlem14  31658  poimirlem17  31661  poimirlem18  31662  poimirlem20  31664  poimirlem21  31665  poimirlem22  31666  poimirlem24  31668  poimirlem25  31669  poimirlem26  31670  poimirlem27  31671  poimirlem28  31672  poimirlem29  31673  poimirlem31  31675  poimirlem32  31676  poimir  31677  mblfinlem3  31683  mblfinlem4  31684  ismblfin  31685  mbfresfi  31691  itg2addnclem  31697  itg2addnclem3  31699  itg2addnc  31700  ftc1anclem7  31727  ftc1anc  31729  areacirclem5  31740  unirep  31743  fnopabeqd  31750  fdc  31778  fdc1  31779  istotbnd  31805  heibor1lem  31845  heibor  31857  isriscg  31927  iscringd  31936  isidlc  31952  prtlem16  32149  prtlem15  32155  fsumshftd  32232  fsumshftdOLD  32233  lsmsat  32283  lsmsatcv  32285  islshpat  32292  lcvfbr  32295  lcvbr  32296  lsatcv0  32306  islshpkrN  32395  cvrval  32544  cvrval2  32549  cvrnbtwn2  32550  cvlexch1  32603  hlsuprexch  32655  cvrval5  32689  cvrat  32696  cvrat42  32718  3dim0  32731  3dim2  32742  islpln3  32807  islpln5  32809  islvol3  32850  islvol5  32853  4atlem11  32883  lineset  33012  isline  33013  ispsubsp2  33020  isline2  33048  isline3  33050  elpaddat  33078  elpadd2at  33080  dalawlem15  33159  pclfinclN  33224  4atex  33350  4atex2  33351  4atex3  33355  ltrnu  33395  cdleme0nex  33565  cdleme31so  33655  cdleme31fv  33666  cdleme31fv2  33669  cdlemefrs29pre00  33671  cdlemefrs29cpre1  33674  cdlemftr3  33841  cdlemb3  33882  cdlemg6d  33897  cdlemg33b  33983  cdlemg33c  33984  cdlemg33e  33986  cdlemk42  34217  dvhopellsm  34394  dibelval3  34424  diblsmopel  34448  diclspsn  34471  dihval  34509  dihopelvalcpre  34525  dih1dimatlem  34606  dihglb2  34619  dochkrshp3  34665  dihjatcclem4  34698  dihjat1lem  34705  mapdval  34905  mapdpglem30  34979  ismrcd1  35249  ismrcd2  35250  mzpcompact2lem  35302  eldioph  35309  eldioph2  35313  eldioph2b  35314  eldioph3  35317  diophin  35324  diophun  35325  diophrex  35327  rexrabdioph  35346  fphpd  35368  fphpdo  35369  pellexlem3  35385  monotuz  35499  monotoddzzfi  35500  monotoddzz  35501  oddcomabszz  35502  jm2.27  35573  rmydioph  35579  expdiophlem1  35586  expdiophlem2  35587  aomclem6  35627  aomclem8  35629  islssfg  35638  islssfg2  35639  hbtlem2  35693  hbtlem4  35695  hbtlem5  35697  hbtlem6  35698  dgraaval  35713  flcidc  35743  ifpbi3  35814  dfhe3  36011  dvgrat  36302  cvgdvgrat  36303  binomcxplemnotnn0  36346  2sbc6g  36407  2sbc5g  36408  iotasbc2  36412  pm14.122a  36414  pm14.123a  36417  fiiuncl  37052  disjf1  37084  disjinfi  37095  monoords  37127  fperiodmullem  37134  supxrgere  37169  supxrgelem  37173  supxrge  37174  fsumclf  37224  fsumsplitf  37225  fsummulc1f  37226  fsumnncl  37229  fsumsplit1  37230  fsumf1of  37232  fmul01  37234  fmuldfeqlem1  37236  fmuldfeq  37237  fmul01lt1lem1  37238  fmul01lt1lem2  37239  fprodexp  37250  fprodabs2  37251  climmulf  37258  climexp  37259  climsuse  37263  climrecf  37264  climinff  37266  climinffOLD  37267  climaddf  37271  mullimc  37272  limcdm0  37274  climf  37278  mullimcf  37279  constlimc  37280  idlimc  37282  limcperiod  37284  sumnnodd  37286  clim2f  37292  limcleqr  37301  neglimc  37304  addlimc  37305  0ellimcdiv  37306  cncfshift  37327  cncfperiod  37332  icccncfext  37341  fprodcncf  37355  fperdvper  37366  ioodvbdlimc1lem2  37380  ioodvbdlimc2lem  37382  dvmptmulf  37385  dvnmptdivc  37386  dvnmul  37391  dvmptfprod  37393  dvnprodlem1  37394  dvnprodlem2  37395  iblspltprt  37423  itgspltprt  37429  stoweidlem3  37436  stoweidlem4  37437  stoweidlem7  37440  stoweidlem15  37448  stoweidlem16  37449  stoweidlem17  37450  stoweidlem19  37452  stoweidlem20  37453  stoweidlem22  37455  stoweidlem23  37456  stoweidlem27  37460  stoweidlem30  37464  stoweidlem32  37466  stoweidlem34  37468  stoweidlem42  37476  stoweidlem43  37477  stoweidlem48  37482  stoweidlem51  37485  stoweidlem59  37493  stoweidlem60  37494  dirkercncflem2  37539  fourierdlem2  37544  fourierdlem3  37545  fourierdlem11  37553  fourierdlem12  37554  fourierdlem15  37557  fourierdlem16  37558  fourierdlem21  37563  fourierdlem34  37576  fourierdlem41  37583  fourierdlem42  37584  fourierdlem46  37588  fourierdlem48  37590  fourierdlem49  37591  fourierdlem50  37592  fourierdlem51  37593  fourierdlem54  37596  fourierdlem68  37610  fourierdlem71  37613  fourierdlem72  37614  fourierdlem73  37615  fourierdlem76  37618  fourierdlem79  37621  fourierdlem81  37623  fourierdlem83  37625  fourierdlem86  37628  fourierdlem87  37629  fourierdlem89  37631  fourierdlem90  37632  fourierdlem91  37633  fourierdlem92  37634  fourierdlem94  37636  fourierdlem97  37639  fourierdlem103  37645  fourierdlem104  37646  fourierdlem107  37649  fourierdlem111  37653  fourierdlem112  37654  fourierdlem113  37655  etransclem2  37672  etransclem46  37716  intsaluni  37739  sge0f1o  37762  sge0lempt  37790  sge0iunmptlemfi  37793  sge0p1  37794  sge0fodjrnlem  37796  sge0iunmpt  37798  meadjiun  37817  2reu4a  38014  iccpartgt  38144  isgboa  38257  nnsum3primes4  38286  nnsum3primesprm  38288  nnsum3primesgbe  38290  nnsum3primesle9  38292  bgoldbachlt  38309  tgoldbachlt  38312  pfxsuff1eqwrdeq  38351  isfusgracl  38509  rngcinv  38754  rngcinvALTV  38766  ringcinv  38805  ringcinvALTV  38829  opeliun2xp  38887  mpt2mptx2  38889  lcoval  38978  lco0  38993  islinindfis  39015  snlindsntor  39037  nnlog2ge0lt1  39151
  Copyright terms: Public domain W3C validator