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

Theorem anbi2d 701
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 637 1  |-  ( ph  ->  ( ( th  /\  ps )  <->  ( th  /\  ch ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367
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 369
This theorem is referenced by:  anbi2  705  anbi12d  708  bi2anan9  871  2eu6OLD  2381  eleq2dALT  2525  eleq2OLD  2529  ceqsex2  3144  ceqsex6v  3148  vtocl2gaf  3171  vtocl4ga  3176  ceqsrex2v  3232  moeq3  3273  mob2  3276  eqreu  3288  reu2eqd  3293  nelrdva  3306  undif4  3871  r19.27z  3916  r19.27zv  3917  ssunsn2  4175  preq12bg  4195  prel12g  4196  opeq2  4204  ralunsn  4223  intab  4302  disjxun  4437  opabbid  4501  opthg  4712  pocl  4796  isso2i  4821  ordelord  4889  ordtri4  4904  xpeq2  5003  rabxp  5025  vtoclr  5033  opeliunxp  5040  posn  5057  opbrop  5068  elrnmpt1  5240  dfres2  5314  brcodir  5374  poltletr  5387  xp11  5427  fununi  5636  fneq2  5652  fnun  5669  feq3  5697  foeq3  5775  funbrfv  5886  ssimaexg  5914  fvopab3g  5927  fvopab3ig  5928  fvelrn  6000  fvcofneq  6015  fmptco  6040  elunirn  6138  f12dfv  6154  f13dfv  6155  isoeq2  6191  isoeq3  6192  isoini  6209  isopolem  6216  f1oiso  6222  f1oiso2  6223  riotabidv  6234  oprabv  6318  oprabbid  6323  cbvoprab3  6346  mpt2mptx  6366  mpt2fun  6377  elrnmpt2res  6389  ov  6395  ov3  6412  ov6g  6413  ovg  6414  caoftrn  6548  dfwe2  6590  dflim4  6656  tfisi  6666  elxp4  6717  elxp5  6718  f1o2ndf1  6881  frxp  6883  xporderlem  6884  fnwelem  6888  brtpos2  6953  dftpos4  6966  onfununi  7004  recseq  7035  omopth  7299  brecop  7396  eroveu  7398  erovlem  7399  erov  7400  ecopovtrn  7406  elpmg  7427  ixpsnval  7465  ixpsnf1o  7502  domeng  7523  dom2lem  7548  xpcomco  7600  xpassen  7604  xpdom2  7605  omxpenlem  7611  xpf1o  7672  unxpdom  7720  isinf  7726  findcard2  7752  findcard2d  7754  fiint  7789  supeq2  7899  wemapso2lem  7970  inf0  8029  cantnfp1lem3  8090  cantnfp1  8091  scott0  8295  isinffi  8364  isacn  8416  aceq1  8489  aceq0  8490  aceq2  8491  dfac3  8493  dfac5lem1  8495  dfac2  8502  dfac12lem2  8515  kmlem8  8528  kmlem14  8534  infmap2  8589  cfval  8618  cflim3  8633  sornom  8648  infpssrlem4  8677  isf32lem9  8732  domtriomlem  8813  axdc2lem  8819  zfac  8831  ac6num  8850  axrepndlem1  8958  axunndlem1  8961  axregnd  8970  axregndOLD  8971  axinfndlem1  8972  axacndlem4  8977  axacndlem5  8978  zfcndac  8986  fpwwe2lem5  9001  pwfseqlem4a  9028  pwfseqlem4  9029  alephgch  9041  wunex2  9105  tskord  9147  nqereu  9296  ordpipq  9309  prcdnq  9360  prnmax  9362  genpnnp  9372  distrlem5pr  9394  ltprord  9397  ltexprlem3  9405  ltexprlem4  9406  ltexpri  9410  prlem936  9414  reclem2pr  9415  addsrmo  9439  mulsrmo  9440  addsrpr  9441  mulsrpr  9442  ltsosr  9460  mulgt0sr  9471  ltresr  9506  axpre-lttrn  9532  axpre-mulgt0  9534  eqlelt  9661  lesub0  10065  wloglei  10081  mulle0b  10409  sup3  10495  infm3  10497  prime  10939  fzind  10958  uzwo  11145  uzwoOLD  11146  zbtwnre  11181  xltnegi  11418  xmulneg1  11464  ixxval  11540  fzval  11677  elfzm11  11753  elfzo  11806  seqof2  12147  nn0opth2  12334  facwordi  12349  hashnn0n0nn  12442  brfi1uzind  12516  2swrd1eqwrdeq  12670  wrd2ind  12694  cshwcsh2id  12787  2swrd2eqwrdeq  12882  relexpsucnnr  12942  relexprelg  12953  relexpindlem  12978  shftfval  12985  shftfib  12987  shftfn  12988  2shfti  12995  abs1m  13250  cau3lem  13269  caubnd2  13272  clim  13399  rlim  13400  clim2  13409  climi  13415  o1lo1  13442  rlimcn2  13495  climcn2  13497  addcn2  13498  subcn2  13499  mulcn2  13500  o1of2  13517  isercoll  13572  caurcvg2  13582  sumeq2w  13596  sumeq2ii  13597  summo  13621  fsum  13624  prodfdiv  13787  ntrivcvgn0  13789  ntrivcvgmullem  13792  prodeq1f  13797  prodeq2w  13801  prodeq2ii  13802  prodmo  13825  zprod  13826  fprod  13830  fprodntriv  13831  sinbnd  13997  cosbnd  13998  divalgb  14146  ndvdssub  14149  smupp1  14214  smueqlem  14224  gcdval  14230  gcdcllem2  14234  gcdneg  14248  gcdass  14267  algcvgblem  14290  prmind2  14312  qredeq  14331  euclemma  14333  qnumval  14354  qdenval  14355  eulerthlem2  14396  pceu  14454  pczpre  14455  pcdiv  14460  prmpwdvds  14506  prmreclem5  14522  vdwapun  14576  ramub2  14616  rami  14617  ramcl  14631  ismred2  15092  isacs  15140  iscatd2  15170  catpropd  15197  oppccatid  15207  isinv  15248  isssc  15308  funcres2b  15385  funcpropd  15388  fucinv  15461  yoniso  15753  prslem  15759  drsdir  15763  drsdirfi  15766  posi  15778  isposd  15784  pltval  15789  plttr  15799  isipodrs  15990  ipodrsima  15994  dirge  16066  gsumpropd  16098  gsumress  16102  mnd1OLD  16161  mrcmndind  16196  mgmnsgrpex  16248  qusgrp2  16387  resscntz  16568  psgnunilem3  16720  psgneu  16730  psgnvali  16732  psgnvalii  16733  isslw  16827  subgslw  16835  iscmnd  17009  gsumval3eu  17106  gsumval3OLD  17107  gsumval3lem2  17109  telgsumfzs  17213  dmdprd  17224  subgdmdprd  17276  dprd2d2  17288  pgpfac1  17326  pgpfaclem2  17328  pgpfaclem3  17329  pgpfac  17330  ablfaclem1  17331  qusring2  17464  dvdsrval  17489  crngunit  17506  dfrhm2  17561  isdrngd  17616  abvpropd  17686  islmod  17711  lssacs  17808  lsspropd  17858  islmhm  17868  lbspropd  17940  ixpsnbasval  18050  fiidomfld  18152  ltbval  18331  opsrval  18334  mpfind  18400  coe1fzgsumd  18539  pf1ind  18586  evl1gsumd  18588  psgndiflemA  18810  pjfval2  18913  frlmup1  19000  scmatf1  19200  mdetralt  19277  mdetralt2  19278  mdetunilem1  19281  mdetunilem2  19282  mdetunilem9  19289  gsummatr01  19328  eltopspOLD  19586  istpsOLD  19588  basis2  19619  eltg2  19626  isclo  19755  isnei  19771  isneip  19773  neiptopnei  19800  restbas  19826  restcld  19840  neitr  19848  iscnp  19905  iscnp3  19912  tgcn  19920  cnpimaex  19924  lmbrf  19928  cncnp  19948  cnprest2  19958  isreg  20000  regsep  20002  isnrm  20003  ist1-2  20015  nrmsep3  20023  isnrm2  20026  hauscmplem  20073  dfcon2  20086  is1stc  20108  1stcclb  20111  1stcfb  20112  is2ndc  20113  2ndc1stc  20118  1stcrest  20120  2ndcsep  20126  1stccnp  20129  islly  20135  llyeq  20137  llyi  20141  hausllycmp  20161  lly1stc  20163  islocfin  20184  txbas  20234  ptpjpre1  20238  elpt  20239  txcnpi  20275  ptpjopn  20279  ptcldmpt  20281  ptclsg  20282  txcnp  20287  ptcnp  20289  hausdiag  20312  tx1stc  20317  xkoinjcn  20354  imasnopn  20357  imasncld  20358  imasncls  20359  fbfinnfr  20508  snfil  20531  uffix2  20591  elfm  20614  elfm2  20615  fmco  20628  hauspwpwf1  20654  flfnei  20658  isflf  20660  lmflf  20672  fclscf  20692  isfcf  20701  alexsublem  20710  cnextcn  20733  cnextfres  20734  eltsms  20797  tsmsresOLD  20811  tsmsres  20812  tsmsf1o  20813  ustuqtop4  20913  ispsmet  20974  ismet  20992  isxmet  20993  ismet2  21002  imasdsf1olem  21042  blres  21100  met2ndc  21192  metcnp3  21209  nrmmetd  21261  pi1grplem  21715  lmmbr2  21864  lmmbrf  21867  iscau2  21882  iscau4  21884  caucfil  21888  lmclim  21907  cfilucfil3OLD  21923  cfilucfil3  21924  bcthlem1  21929  bcth  21934  ishl2  21976  pmltpclem1  22026  elovolm  22052  ovolgelb  22057  ovolicc  22100  mbfaddlem  22233  i1fres  22278  mbfi1fseqlem4  22291  itg2l  22302  itg2leub  22307  itg2seq  22315  isibl  22338  iblitg  22341  dfitg  22342  itgeq2  22350  itgvallem  22357  iblcnlem1  22360  iblrelem  22363  iblpos  22365  ellimc3  22449  limciun  22464  limcun  22465  dvmptfsum  22542  dveflem  22546  lhop1lem  22580  dvfsumlem2  22594  dvfsumlem4  22596  mdegleb  22630  elply2  22759  plypf1  22775  coeval  22786  plydivlem4  22858  sincosq3sgn  23059  vmasum  23689  lgsqrlem1  23814  lgsquadlem1  23827  2sqlem8  23845  2sqlem9  23846  2sqlem11  23848  dchrisumlema  23871  dchrisumlem2  23873  pntibndlem3  23975  pntibnd  23976  pntleme  23991  pntlemp  23993  axtgsegcon  24059  axtg5seg  24060  axtgpasch  24062  iscgrg  24105  legov  24173  ltgov  24184  ishlg  24187  mirreu3  24236  israg  24275  islnopp  24314  ishpg  24329  iscgra  24370  brcgr  24405  brbtwn2  24410  colinearalg  24415  ax5seg  24443  axcontlem5  24473  axcontlem10  24478  usgraedg4  24589  cusgrafilem2  24682  cusgrafi  24684  uvtx01vtx  24694  usgrnloop  24767  spthonepeq  24791  usgra2adedgwlkonALT  24818  usgra2wlkspthlem1  24821  usgrcyclnl2  24843  4cycl4v4e  24868  4cycl4dv4e  24870  wwlk  24883  wlklniswwlkn2  24902  clwlkisclwwlklem0  24990  clwlkisclwwlk  24991  eleclclwwlkn  25035  usghashecclwwlk  25037  el2wlkonot  25071  el2spthonot  25072  el2spthonot0  25073  usg2spthonot  25090  usg2spthonot0  25091  usg2spthonot1  25092  isrusgra  25129  isrusgusrg  25134  isrgrac  25136  isrusgrac  25137  rusgranumwlkl1  25149  iseupa  25167  eupath2lem3  25181  1vwmgra  25205  3vfriswmgra  25207  3cyclfrgrarn1  25214  4cycl2vnunb  25219  vdn1frgrav2  25227  vdgn1frgrav2  25228  frgrancvvdeqlemB  25240  usg2spot2nb  25267  usgreg2spot  25269  2spotmdisj  25270  usgreghash2spot  25271  extwwlkfab  25292  numclwwlk2lem1  25304  numclwwlk5  25314  isgrpo  25396  isgrp2d  25435  isgrpda  25497  ismndo  25543  drngoi  25607  vci  25639  isvclem  25668  nmoofval  25875  nmooval  25876  nmosetn0  25878  nmoolb  25884  nmoubi  25885  nmoo0  25904  nmlno0lem  25906  isphg  25930  norm3lemt  26267  chlimi  26350  ocsh  26399  cmbr  26700  chscllem2  26754  spansncv  26769  eigorth  26955  nmopval  26973  nmopsetn0  26982  nmfnval  26993  nmfnsetn0  26995  nmoplb  27024  nmfnlb  27041  nmopnegi  27082  nmop0  27103  nmfn0  27104  nmlnop0iALT  27112  nmopun  27131  nmcexi  27143  branmfn  27222  leopmuli  27250  pjnmopi  27265  cvbr  27399  mdbr  27411  dmdbr  27416  atom1d  27470  chrelat2  27487  atcvati  27503  atord  27505  atcvat2  27506  chirredlem4  27510  mdsymlem5  27524  disjunsn  27664  opeldifid  27670  fcoinvbr  27675  fimarab  27704  fmptcof2  27724  aciunf1lem  27729  ofpreima  27734  funcnv4mpt  27739  mpt2mptxf  27746  2ndpreima  27754  f1od2  27778  fpwrelmapffslem  27786  xeqlelt  27821  ishashinf  27840  ressprs  27877  isomnd  27925  archiabllem2a  27972  archiabl  27976  isslmd  27979  gsumle  28004  gsumvsca1  28008  gsumvsca2  28009  orngmul  28028  ismntop  28238  esumcvg  28315  sitgval  28538  eulerpartlemmf  28578  eulerpartlemgvv  28579  eulerpartlemn  28584  eulerpart  28585  brafs  28816  lgamgulmlem2  28836  erdszelem3  28901  erdsze  28910  pconcn  28933  cnpcon  28939  txpcon  28941  conpcon  28944  cvmscbv  28967  iscvm  28968  cvmsi  28974  cvmsval  28975  mclsval  29187  mclsppslem  29207  elima4  29449  dfrdg2  29468  dfrdg3  29469  elpred  29497  trpredrec  29561  poseq  29573  soseq  29574  sltval  29647  nocvxminlem  29690  nofulllem1  29702  elfuns  29793  brimg  29815  brsuccf  29819  dfrdg4  29828  tfrqfree  29829  brofs  29883  funtransport  29909  fvtransport  29910  brifs  29921  lineext  29954  brfs  29957  btwnconn1lem11  29975  btwnconn1lem14  29978  brsegle  29986  segletr  29992  segleantisym  29993  seglelin  29994  funray  30018  fvray  30019  funline  30020  fvline  30022  ellines  30030  linethru  30031  ptrest  30288  mblfinlem3  30293  mblfinlem4  30294  ismblfin  30295  mbfresfi  30301  itg2addnclem  30306  itg2addnclem3  30308  itg2addnc  30309  ftc1anclem7  30336  ftc1anc  30338  areacirclem5  30351  trer  30374  opnrebl2  30379  nn0prpwlem  30380  isfne4  30398  isfne2  30400  isfne3  30401  unirep  30443  fnopabeqd  30450  fdc  30478  fdc1  30479  istotbnd  30505  heibor1lem  30545  heibor  30557  isriscg  30627  iscringd  30636  isidlc  30652  prtlem16  30850  prtlem15  30856  ismrcd1  30870  ismrcd2  30871  mzpcompact2lem  30923  eldioph  30930  eldioph2  30934  eldioph2b  30935  eldioph3  30938  diophin  30945  diophun  30946  diophrex  30948  rexrabdioph  30967  fphpd  30989  fphpdo  30990  pellexlem3  31006  monotuz  31116  monotoddzzfi  31117  monotoddzz  31118  oddcomabszz  31119  jm2.27  31189  rmydioph  31195  expdiophlem1  31202  expdiophlem2  31203  aomclem6  31244  aomclem8  31246  islssfg  31255  islssfg2  31256  hbtlem2  31314  hbtlem4  31316  hbtlem5  31318  hbtlem6  31319  dgraaval  31334  flcidc  31364  dvgrat  31434  cvgdvgrat  31435  lcmval  31439  lcmneg  31450  lcmgcdlem  31453  lcmass  31459  binomcxplemnotnn0  31502  2sbc6g  31563  2sbc5g  31564  iotasbc2  31568  pm14.122a  31570  pm14.123a  31573  monoords  31735  fperiodmullem  31742  fsumclf  31806  fsumsplitf  31807  fsummulc1f  31808  fsumnncl  31811  fsumsplit1  31812  fmul01  31813  fmuldfeqlem1  31815  fmuldfeq  31816  fmul01lt1lem1  31817  fmul01lt1lem2  31818  fproddivf  31827  fprodsplitf  31828  fprodsplit1f  31832  fprodexp  31839  fprodabs2  31841  climmulf  31849  climexp  31850  climsuse  31853  climrecf  31854  climinff  31856  climaddf  31860  mullimc  31861  limcdm0  31863  climf  31867  mullimcf  31868  constlimc  31869  idlimc  31871  limcperiod  31873  sumnnodd  31875  clim2f  31881  limcleqr  31889  neglimc  31892  addlimc  31893  0ellimcdiv  31894  cncfshift  31915  cncfperiod  31920  icccncfext  31929  fprodcncf  31943  fperdvper  31954  ioodvbdlimc1lem2  31968  ioodvbdlimc2lem  31970  dvmptmulf  31973  dvnmptdivc  31974  dvnmul  31979  dvmptfprod  31981  dvnprodlem1  31982  dvnprodlem2  31983  iblspltprt  32011  itgspltprt  32017  stoweidlem3  32024  stoweidlem4  32025  stoweidlem7  32028  stoweidlem15  32036  stoweidlem16  32037  stoweidlem17  32038  stoweidlem19  32040  stoweidlem20  32041  stoweidlem22  32043  stoweidlem23  32044  stoweidlem27  32048  stoweidlem30  32051  stoweidlem32  32053  stoweidlem34  32055  stoweidlem42  32063  stoweidlem43  32064  stoweidlem48  32069  stoweidlem51  32072  stoweidlem59  32080  stoweidlem60  32081  dirkercncflem2  32125  fourierdlem2  32130  fourierdlem3  32131  fourierdlem11  32139  fourierdlem12  32140  fourierdlem15  32143  fourierdlem16  32144  fourierdlem21  32149  fourierdlem34  32162  fourierdlem41  32169  fourierdlem42  32170  fourierdlem46  32174  fourierdlem48  32176  fourierdlem49  32177  fourierdlem50  32178  fourierdlem51  32179  fourierdlem54  32182  fourierdlem68  32196  fourierdlem71  32199  fourierdlem72  32200  fourierdlem73  32201  fourierdlem76  32204  fourierdlem79  32207  fourierdlem81  32209  fourierdlem83  32211  fourierdlem86  32214  fourierdlem87  32215  fourierdlem89  32217  fourierdlem90  32218  fourierdlem91  32219  fourierdlem92  32220  fourierdlem94  32222  fourierdlem97  32225  fourierdlem103  32231  fourierdlem104  32232  fourierdlem107  32235  fourierdlem111  32239  fourierdlem112  32240  fourierdlem113  32241  etransclem2  32258  etransclem46  32302  2reu4a  32433  pfxsuff1eqwrdeq  32635  isfusgracl  32798  rngcinv  33043  rngcinvALTV  33055  ringcinv  33094  ringcinvALTV  33118  opeliun2xp  33176  mpt2mptx2  33178  lcoval  33267  lco0  33282  islinindfis  33304  snlindsntor  33326  nnlog2ge0lt1  33441  bnj976  34237  bnj852  34380  bnj1014  34419  bnj1015  34420  bnj1118  34441  bnj1123  34443  bnj1148  34453  bnj1171  34457  bnj1373  34487  bnj1489  34513  bj-eleq2w  34824  bj-finsumval0  35063  fsumshftd  35079  fsumshftdOLD  35080  lsmsat  35130  lsmsatcv  35132  islshpat  35139  lcvfbr  35142  lcvbr  35143  lsatcv0  35153  islshpkrN  35242  cvrval  35391  cvrval2  35396  cvrnbtwn2  35397  cvlexch1  35450  hlsuprexch  35502  cvrval5  35536  cvrat  35543  cvrat42  35565  3dim0  35578  3dim2  35589  islpln3  35654  islpln5  35656  islvol3  35697  islvol5  35700  4atlem11  35730  lineset  35859  isline  35860  ispsubsp2  35867  isline2  35895  isline3  35897  elpaddat  35925  elpadd2at  35927  dalawlem15  36006  pclfinclN  36071  4atex  36197  4atex2  36198  4atex3  36202  ltrnu  36242  cdleme0nex  36412  cdleme31so  36502  cdleme31fv  36513  cdleme31fv2  36516  cdlemefrs29pre00  36518  cdlemefrs29cpre1  36521  cdlemftr3  36688  cdlemb3  36729  cdlemg6d  36744  cdlemg33b  36830  cdlemg33c  36831  cdlemg33e  36833  cdlemk42  37064  dvhopellsm  37241  dibelval3  37271  diblsmopel  37295  diclspsn  37318  dihval  37356  dihopelvalcpre  37372  dih1dimatlem  37453  dihglb2  37466  dochkrshp3  37512  dihjatcclem4  37545  dihjat1lem  37552  mapdval  37752  mapdpglem30  37826  ifpbi3  38098  dfhe3  38249
  Copyright terms: Public domain W3C validator