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

Theorem anbi2d 685
Description: Deduction adding a left conjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-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 23 . 2  |-  ( ph  ->  ( th  ->  ( ps 
<->  ch ) ) )
32pm5.32d 621 1  |-  ( ph  ->  ( ( th  /\  ps )  <->  ( th  /\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  anbi2  689  anbi12d  692  bi2anan9  844  2eu6  2339  eleq2  2465  ceqsex2  2952  ceqsex6v  2956  vtocl2gaf  2978  ceqsrex2v  3031  moeq3  3071  mob2  3074  eqreu  3086  nelrdva  3103  undif4  3644  r19.27z  3686  r19.27zv  3687  ssunsn2  3918  preq12bg  3937  opeq2  3945  ralunsn  3963  intab  4040  disjxun  4170  opabbid  4230  opthg  4396  pocl  4470  isso2i  4495  ordelord  4563  ordtri4  4578  dfwe2  4721  dflim4  4787  tfisi  4797  xpeq2  4852  rabxp  4873  vtoclr  4881  opeliunxp  4888  posn  4905  opbrop  4914  elrnmpt1  5078  dfres2  5152  brcodir  5212  poltletr  5228  xp11  5263  elxp4  5316  elxp5  5317  fununi  5476  fneq2  5494  fnun  5510  feq3  5537  foeq3  5610  funbrfv  5724  ssimaexg  5748  fvopab3g  5761  fvopab3ig  5762  fvelrn  5825  fmptco  5860  elunirnALT  5959  isoeq2  5999  isoeq3  6000  isoini  6017  isopolem  6024  f1oiso  6030  f1oiso2  6031  oprabbid  6086  cbvoprab3  6107  mpt2mptx  6123  mpt2fun  6131  ov  6152  ov3  6169  ov6g  6170  ovg  6171  caoftrn  6298  f1o2ndf1  6413  frxp  6415  xporderlem  6416  fnwelem  6420  brtpos2  6444  dftpos4  6457  riotabidv  6510  onfununi  6562  recseq  6593  tfrlem1  6595  omopth  6860  brecop  6956  eroveu  6958  erovlem  6959  erov  6960  ecopovtrn  6966  th3qlem1  6969  th3qlem2  6970  th3q  6972  elpmg  6991  ixpsnf1o  7061  domeng  7081  dom2lem  7106  xpcomco  7157  xpassen  7161  xpdom2  7162  omxpenlem  7168  xpf1o  7228  unxpdom  7275  isinf  7281  findcard2  7307  fiint  7342  supeq2  7411  inf0  7532  scott0  7766  isinffi  7835  isacn  7881  aceq1  7954  aceq0  7955  aceq2  7956  dfac3  7958  dfac5lem1  7960  dfac2  7967  dfac12lem2  7980  kmlem8  7993  kmlem14  7999  infmap2  8054  cfval  8083  cflim3  8098  sornom  8113  infpssrlem4  8142  isf32lem9  8197  domtriomlem  8278  axdc2lem  8284  zfac  8296  ac6num  8315  axrepndlem1  8423  axunndlem1  8426  axregnd  8435  axinfndlem1  8436  axacndlem4  8441  axacndlem5  8442  zfcndac  8450  fpwwe2lem5  8465  pwfseqlem4a  8492  pwfseqlem4  8493  alephgch  8509  wunex2  8569  tskord  8611  nqereu  8762  ordpipq  8775  prcdnq  8826  prnmax  8828  genpnnp  8838  distrlem5pr  8860  ltprord  8863  ltexprlem3  8871  ltexprlem4  8872  ltexpri  8876  prlem936  8880  reclem2pr  8881  ltsosr  8925  mulgt0sr  8936  ltresr  8971  axpre-lttrn  8997  axpre-mulgt0  8999  eqlelt  9118  lesub0  9500  wloglei  9515  sup3  9921  infm3  9923  prime  10306  fzind  10324  uzwo  10495  uzwoOLD  10496  zbtwnre  10528  xltnegi  10758  xmulneg1  10804  ixxval  10880  fzval  11001  elfzm11  11071  elfzo  11097  seqof2  11336  nn0opth2  11520  facwordi  11535  hashnn0n0nn  11619  brfi1uzind  11670  shftfval  11840  shftfib  11842  shftfn  11843  2shfti  11850  abs1m  12094  cau3lem  12113  caubnd2  12116  clim  12243  rlim  12244  clim2  12253  climi  12259  o1lo1  12286  rlimcn2  12339  climcn2  12341  addcn2  12342  subcn2  12343  mulcn2  12344  o1of2  12361  isercoll  12416  caurcvg2  12426  sumeq2w  12441  sumeq2ii  12442  cbvsum  12444  summo  12466  fsum  12469  sinbnd  12736  cosbnd  12737  divalgb  12879  ndvdssub  12882  smupp1  12947  smueqlem  12957  gcdval  12963  gcdcllem2  12967  gcdneg  12981  gcdass  13000  algcvgblem  13023  prmind2  13045  qredeq  13061  euclemma  13063  qnumval  13084  qdenval  13085  eulerthlem2  13126  pceu  13175  pczpre  13176  pcdiv  13181  prmpwdvds  13227  prmreclem5  13243  vdwapun  13297  ramub2  13337  rami  13338  ramcl  13352  ismred2  13783  isacs  13831  iscatd2  13861  catpropd  13890  oppccatid  13900  isinv  13940  isssc  13975  funcres2b  14049  funcpropd  14052  fucinv  14125  yoniso  14337  prslem  14343  drsdir  14347  drsdirfi  14350  posi  14362  isposd  14367  pltval  14372  plttr  14382  isipodrs  14542  ipodrsima  14546  spwval  14612  dirge  14637  mndlem1  14649  gsumpropd  14731  gsumress  14732  divsgrp2  14891  resscntz  15085  isslw  15197  subgslw  15205  iscmnd  15379  gsumval3eu  15468  gsumval3  15469  dmdprd  15514  subgdmdprd  15547  dprd2d2  15557  pgpfac1  15593  pgpfaclem2  15595  pgpfaclem3  15596  pgpfac  15597  ablfaclem1  15598  divsrng2  15681  dvdsrval  15705  crngunit  15722  dfrhm2  15776  isdrngd  15815  abvpropd  15885  islmod  15909  lssacs  15998  lsspropd  16048  islmhm  16058  lbspropd  16126  fiidomfld  16323  ltbval  16487  opsrval  16490  pjfval2  16891  eltopspOLD  16938  istpsOLD  16940  basis2  16971  eltg2  16978  isclo  17106  isnei  17122  isneip  17124  neiptopnei  17151  restbas  17176  restcld  17190  neitr  17198  iscnp  17255  iscnp3  17262  tgcn  17270  cnpimaex  17274  lmbrf  17278  cncnp  17298  cnprest2  17308  isreg  17350  regsep  17352  isnrm  17353  ist1-2  17365  nrmsep3  17373  isnrm2  17376  hauscmplem  17423  dfcon2  17435  is1stc  17457  1stcclb  17460  1stcfb  17461  is2ndc  17462  2ndc1stc  17467  1stcrest  17469  2ndcsep  17475  1stccnp  17478  islly  17484  llyeq  17486  llyi  17490  hausllycmp  17510  lly1stc  17512  txbas  17552  ptpjpre1  17556  elpt  17557  txcnpi  17593  ptpjopn  17597  ptcldmpt  17599  ptclsg  17600  txcnp  17605  ptcnp  17607  hausdiag  17630  tx1stc  17635  xkoinjcn  17672  imasnopn  17675  imasncld  17676  imasncls  17677  fbfinnfr  17826  snfil  17849  uffix2  17909  elfm  17932  elfm2  17933  fmco  17946  hauspwpwf1  17972  flfnei  17976  isflf  17978  lmflf  17990  fclscf  18010  isfcf  18019  alexsublem  18028  cnextcn  18051  cnextfres  18052  eltsms  18115  tsmsres  18126  tsmsf1o  18127  ustuqtop4  18227  ispsmet  18288  ismet  18306  isxmet  18307  ismet2  18316  imasdsf1olem  18356  blres  18414  met2ndc  18506  metcnp3  18523  nrmmetd  18575  pi1grplem  19027  lmmbr2  19165  lmmbrf  19168  iscau2  19183  iscau4  19185  caucfil  19189  lmclim  19208  cfilucfil3OLD  19224  cfilucfil3  19225  bcthlem1  19230  bcth  19235  ishl2  19277  pmltpclem1  19298  elovolm  19324  ovolgelb  19329  ovolicc  19372  mbfaddlem  19505  i1fres  19550  mbfi1fseqlem4  19563  itg2l  19574  itg2leub  19579  itg2seq  19587  isibl  19610  iblitg  19613  dfitg  19614  itgeq2  19622  itgvallem  19629  iblcnlem1  19632  iblrelem  19635  iblpos  19637  ellimc3  19719  limciun  19734  limcun  19735  dvmptfsum  19812  dveflem  19816  lhop1lem  19850  dvfsumlem2  19864  dvfsumlem4  19866  mpfind  19918  pf1ind  19928  elply2  20068  plypf1  20084  coeval  20095  plydivlem4  20166  sincosq3sgn  20361  vmasum  20953  lgsqrlem1  21078  lgsquadlem1  21091  2sqlem8  21109  2sqlem9  21110  2sqlem11  21112  dchrisumlema  21135  dchrisumlem2  21137  pntibndlem3  21239  pntibnd  21240  pntleme  21255  pntlemp  21257  usgraedg4  21359  cusgrafilem2  21442  cusgrafi  21444  uvtx01vtx  21454  usgrnloop  21516  spthonepeq  21540  usgrcyclnl2  21581  4cycl4v4e  21606  4cycl4dv4e  21608  iseupa  21640  eupath2lem3  21654  isgrpo  21737  isgrp2d  21776  isgrpda  21838  ismndo  21884  drngoi  21948  vci  21980  isvclem  22009  nmoofval  22216  nmooval  22217  nmosetn0  22219  nmoolb  22225  nmoubi  22226  nmoo0  22245  nmlno0lem  22247  isphg  22271  norm3lemt  22607  chlimi  22690  ocsh  22738  cmbr  23039  chscllem2  23093  spansncv  23108  eigorth  23294  nmopval  23312  nmopsetn0  23321  nmfnval  23332  nmfnsetn0  23334  nmoplb  23363  nmfnlb  23380  nmopnegi  23421  nmop0  23442  nmfn0  23443  nmlnop0iALT  23451  nmopun  23470  nmcexi  23482  branmfn  23561  leopmuli  23589  pjnmopi  23604  cvbr  23738  mdbr  23750  dmdbr  23755  atom1d  23809  chrelat2  23826  atcvati  23842  atord  23844  atcvat2  23845  chirredlem4  23849  mdsymlem5  23863  fmptcof2  24029  ofpreima  24034  funcnv4mpt  24038  2ndpreima  24049  xeqlelt  24092  ishashinf  24112  isofld  24188  ofldadd  24191  ofldmul  24192  esumcvg  24429  sitgval  24600  lgamgulmlem2  24767  erdszelem3  24832  erdsze  24841  pconcn  24864  cnpcon  24870  txpcon  24872  conpcon  24875  cvmscbv  24898  iscvm  24899  cvmsi  24905  cvmsval  24906  relexp0  25082  relexpsucr  25083  relexpsucl  25085  relexpadd  25091  relexpindlem  25092  mulle0b  25145  prodfdiv  25177  ntrivcvgn0  25179  ntrivcvgmullem  25182  prodeq1f  25187  prodeq2w  25191  prodeq2ii  25192  prodmo  25215  zprod  25216  fprod  25220  fprodntriv  25221  dfrdg2  25366  dfrdg3  25367  elpred  25391  trpredrec  25455  poseq  25467  soseq  25468  sltval  25515  nocvxminlem  25558  nofulllem1  25570  elfuns  25668  brimg  25690  brsuccf  25694  dfrdg4  25703  tfrqfree  25704  brcgr  25743  brbtwn2  25748  colinearalg  25753  ax5seg  25781  axcontlem5  25811  axcontlem10  25816  brofs  25843  funtransport  25869  fvtransport  25870  brifs  25881  lineext  25914  brfs  25917  btwnconn1lem11  25935  btwnconn1lem14  25938  brsegle  25946  segletr  25952  segleantisym  25953  seglelin  25954  funray  25978  fvray  25979  funline  25980  fvline  25982  ellines  25990  linethru  25991  mblfinlem2  26144  mblfinlem3  26145  ismblfin  26146  mbfresfi  26152  itg2addnclem  26155  itg2addnclem3  26157  itg2addnc  26158  areacirclem6  26186  trer  26209  opnrebl2  26214  nn0prpwlem  26215  isfne4  26239  isfne2  26241  isfne3  26242  islocfin  26266  unirep  26304  fnopabeqd  26311  fdc  26339  fdc1  26340  istotbnd  26368  heibor1lem  26408  heibor  26420  isriscg  26490  iscringd  26499  isidlc  26515  prtlem16  26608  prtlem15  26614  ismrcd1  26642  ismrcd2  26643  mzpcompact2lem  26698  eldioph  26706  eldioph2  26710  eldioph2b  26711  eldioph3  26714  diophin  26721  diophun  26722  diophrex  26724  rexrabdioph  26744  fphpd  26767  fphpdo  26768  pellexlem3  26784  monotuz  26894  monotoddzzfi  26895  monotoddzz  26896  oddcomabszz  26897  jm2.27  26969  rmydioph  26975  expdiophlem1  26982  expdiophlem2  26983  aomclem6  27024  aomclem8  27027  islssfg  27036  islssfg2  27037  frlmup1  27118  hbtlem2  27196  hbtlem4  27198  hbtlem5  27200  hbtlem6  27201  dgraaval  27217  flcidc  27247  psgnunilem3  27287  psgneu  27297  psgnvali  27299  psgnvalii  27300  2sbc6g  27483  2sbc5g  27484  iotasbc2  27488  pm14.122a  27490  pm14.123a  27493  fmul01  27577  fmuldfeqlem1  27579  fmuldfeq  27580  fmul01lt1lem1  27581  fmul01lt1lem2  27582  climmulf  27597  climexp  27598  climsuse  27601  climrecf  27602  climinff  27604  stoweidlem3  27619  stoweidlem4  27620  stoweidlem7  27623  stoweidlem15  27631  stoweidlem16  27632  stoweidlem17  27633  stoweidlem19  27635  stoweidlem20  27636  stoweidlem22  27638  stoweidlem23  27639  stoweidlem27  27643  stoweidlem30  27646  stoweidlem32  27648  stoweidlem34  27650  stoweidlem42  27658  stoweidlem43  27659  stoweidlem48  27664  stoweidlem51  27667  stoweidlem59  27675  stoweidlem60  27676  2reu4a  27834  f12dfv  27961  f13dfv  27962  swrdccatin2  28018  swrdccatin12c  28028  swrdccat3b  28031  usgra2wlkspthlem1  28036  el2wlkonot  28066  el2spthonot  28067  el2spthonot0  28068  usg2spthonot  28085  usg2spthonot0  28086  usg2spthonot1  28087  1vwmgra  28107  3vfriswmgra  28109  3cyclfrgrarn1  28116  4cycl2vnunb  28121  vdn1frgrav2  28130  vdgn1frgrav2  28131  frgrancvvdeqlemB  28141  usg2spot2nb  28168  usgreg2spot  28170  2spotmdisj  28171  usgreghash2spot  28172  bnj976  28854  bnj852  28998  bnj1014  29037  bnj1015  29038  bnj1118  29059  bnj1123  29061  bnj1148  29071  bnj1171  29075  bnj1373  29105  bnj1489  29131  lsmsat  29491  lsmsatcv  29493  islshpat  29500  lcvfbr  29503  lcvbr  29504  lsatcv0  29514  islshpkrN  29603  cvrval  29752  cvrval2  29757  cvrnbtwn2  29758  cvlexch1  29811  hlsuprexch  29863  cvrval5  29897  cvrat  29904  cvrat42  29926  3dim0  29939  3dim2  29950  islpln3  30015  islpln5  30017  islvol3  30058  islvol5  30061  4atlem11  30091  lineset  30220  isline  30221  ispsubsp2  30228  isline2  30256  isline3  30258  elpaddat  30286  elpadd2at  30288  dalawlem15  30367  pclfinclN  30432  4atex  30558  4atex2  30559  4atex3  30563  ltrnu  30603  cdleme0nex  30772  cdleme31so  30861  cdleme31fv  30872  cdleme31fv2  30875  cdlemefrs29pre00  30877  cdlemefrs29cpre1  30880  cdlemftr3  31047  cdlemb3  31088  cdlemg6d  31103  cdlemg33b  31189  cdlemg33c  31190  cdlemg33e  31192  cdlemk42  31423  dvhopellsm  31600  dibelval3  31630  diblsmopel  31654  diclspsn  31677  dihval  31715  dihopelvalcpre  31731  dih1dimatlem  31812  dihglb2  31825  dochkrshp3  31871  dihjatcclem4  31904  dihjat1lem  31911  mapdval  32111  mapdpglem30  32185
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator