MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  anbi2d Structured version   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  2365  eleq2  2496  ceqsex2  2984  ceqsex6v  2988  vtocl2gaf  3010  ceqsrex2v  3063  moeq3  3103  mob2  3106  eqreu  3118  nelrdva  3135  undif4  3676  r19.27z  3718  r19.27zv  3719  ssunsn2  3950  preq12bg  3969  opeq2  3977  ralunsn  3995  intab  4072  disjxun  4202  opabbid  4262  opthg  4428  pocl  4502  isso2i  4527  ordelord  4595  ordtri4  4610  dfwe2  4754  dflim4  4820  tfisi  4830  xpeq2  4885  rabxp  4906  vtoclr  4914  opeliunxp  4921  posn  4938  opbrop  4947  elrnmpt1  5111  dfres2  5185  brcodir  5245  poltletr  5261  xp11  5296  elxp4  5349  elxp5  5350  fununi  5509  fneq2  5527  fnun  5543  feq3  5570  foeq3  5643  funbrfv  5757  ssimaexg  5781  fvopab3g  5794  fvopab3ig  5795  fvelrn  5858  fmptco  5893  elunirnALT  5992  isoeq2  6032  isoeq3  6033  isoini  6050  isopolem  6057  f1oiso  6063  f1oiso2  6064  oprabbid  6119  cbvoprab3  6140  mpt2mptx  6156  mpt2fun  6164  ov  6185  ov3  6202  ov6g  6203  ovg  6204  caoftrn  6331  f1o2ndf1  6446  frxp  6448  xporderlem  6449  fnwelem  6453  brtpos2  6477  dftpos4  6490  riotabidv  6543  onfununi  6595  recseq  6626  tfrlem1  6628  omopth  6893  brecop  6989  eroveu  6991  erovlem  6992  erov  6993  ecopovtrn  6999  th3qlem1  7002  th3qlem2  7003  th3q  7005  elpmg  7024  ixpsnf1o  7094  domeng  7114  dom2lem  7139  xpcomco  7190  xpassen  7194  xpdom2  7195  omxpenlem  7201  xpf1o  7261  unxpdom  7308  isinf  7314  findcard2  7340  fiint  7375  supeq2  7445  inf0  7568  scott0  7802  isinffi  7871  isacn  7917  aceq1  7990  aceq0  7991  aceq2  7992  dfac3  7994  dfac5lem1  7996  dfac2  8003  dfac12lem2  8016  kmlem8  8029  kmlem14  8035  infmap2  8090  cfval  8119  cflim3  8134  sornom  8149  infpssrlem4  8178  isf32lem9  8233  domtriomlem  8314  axdc2lem  8320  zfac  8332  ac6num  8351  axrepndlem1  8459  axunndlem1  8462  axregnd  8471  axinfndlem1  8472  axacndlem4  8477  axacndlem5  8478  zfcndac  8486  fpwwe2lem5  8501  pwfseqlem4a  8528  pwfseqlem4  8529  alephgch  8545  wunex2  8605  tskord  8647  nqereu  8798  ordpipq  8811  prcdnq  8862  prnmax  8864  genpnnp  8874  distrlem5pr  8896  ltprord  8899  ltexprlem3  8907  ltexprlem4  8908  ltexpri  8912  prlem936  8916  reclem2pr  8917  ltsosr  8961  mulgt0sr  8972  ltresr  9007  axpre-lttrn  9033  axpre-mulgt0  9035  eqlelt  9154  lesub0  9536  wloglei  9551  sup3  9957  infm3  9959  prime  10342  fzind  10360  uzwo  10531  uzwoOLD  10532  zbtwnre  10564  xltnegi  10794  xmulneg1  10840  ixxval  10916  fzval  11037  elfzm11  11108  elfzo  11134  seqof2  11373  nn0opth2  11557  facwordi  11572  hashnn0n0nn  11656  brfi1uzind  11707  shftfval  11877  shftfib  11879  shftfn  11880  2shfti  11887  abs1m  12131  cau3lem  12150  caubnd2  12153  clim  12280  rlim  12281  clim2  12290  climi  12296  o1lo1  12323  rlimcn2  12376  climcn2  12378  addcn2  12379  subcn2  12380  mulcn2  12381  o1of2  12398  isercoll  12453  caurcvg2  12463  sumeq2w  12478  sumeq2ii  12479  cbvsum  12481  summo  12503  fsum  12506  sinbnd  12773  cosbnd  12774  divalgb  12916  ndvdssub  12919  smupp1  12984  smueqlem  12994  gcdval  13000  gcdcllem2  13004  gcdneg  13018  gcdass  13037  algcvgblem  13060  prmind2  13082  qredeq  13098  euclemma  13100  qnumval  13121  qdenval  13122  eulerthlem2  13163  pceu  13212  pczpre  13213  pcdiv  13218  prmpwdvds  13264  prmreclem5  13280  vdwapun  13334  ramub2  13374  rami  13375  ramcl  13389  ismred2  13820  isacs  13868  iscatd2  13898  catpropd  13927  oppccatid  13937  isinv  13977  isssc  14012  funcres2b  14086  funcpropd  14089  fucinv  14162  yoniso  14374  prslem  14380  drsdir  14384  drsdirfi  14387  posi  14399  isposd  14404  pltval  14409  plttr  14419  isipodrs  14579  ipodrsima  14583  spwval  14649  dirge  14674  mndlem1  14686  gsumpropd  14768  gsumress  14769  divsgrp2  14928  resscntz  15122  isslw  15234  subgslw  15242  iscmnd  15416  gsumval3eu  15505  gsumval3  15506  dmdprd  15551  subgdmdprd  15584  dprd2d2  15594  pgpfac1  15630  pgpfaclem2  15632  pgpfaclem3  15633  pgpfac  15634  ablfaclem1  15635  divsrng2  15718  dvdsrval  15742  crngunit  15759  dfrhm2  15813  isdrngd  15852  abvpropd  15922  islmod  15946  lssacs  16035  lsspropd  16085  islmhm  16095  lbspropd  16163  fiidomfld  16360  ltbval  16524  opsrval  16527  pjfval2  16928  eltopspOLD  16975  istpsOLD  16977  basis2  17008  eltg2  17015  isclo  17143  isnei  17159  isneip  17161  neiptopnei  17188  restbas  17214  restcld  17228  neitr  17236  iscnp  17293  iscnp3  17300  tgcn  17308  cnpimaex  17312  lmbrf  17316  cncnp  17336  cnprest2  17346  isreg  17388  regsep  17390  isnrm  17391  ist1-2  17403  nrmsep3  17411  isnrm2  17414  hauscmplem  17461  dfcon2  17474  is1stc  17496  1stcclb  17499  1stcfb  17500  is2ndc  17501  2ndc1stc  17506  1stcrest  17508  2ndcsep  17514  1stccnp  17517  islly  17523  llyeq  17525  llyi  17529  hausllycmp  17549  lly1stc  17551  txbas  17591  ptpjpre1  17595  elpt  17596  txcnpi  17632  ptpjopn  17636  ptcldmpt  17638  ptclsg  17639  txcnp  17644  ptcnp  17646  hausdiag  17669  tx1stc  17674  xkoinjcn  17711  imasnopn  17714  imasncld  17715  imasncls  17716  fbfinnfr  17865  snfil  17888  uffix2  17948  elfm  17971  elfm2  17972  fmco  17985  hauspwpwf1  18011  flfnei  18015  isflf  18017  lmflf  18029  fclscf  18049  isfcf  18058  alexsublem  18067  cnextcn  18090  cnextfres  18091  eltsms  18154  tsmsres  18165  tsmsf1o  18166  ustuqtop4  18266  ispsmet  18327  ismet  18345  isxmet  18346  ismet2  18355  imasdsf1olem  18395  blres  18453  met2ndc  18545  metcnp3  18562  nrmmetd  18614  pi1grplem  19066  lmmbr2  19204  lmmbrf  19207  iscau2  19222  iscau4  19224  caucfil  19228  lmclim  19247  cfilucfil3OLD  19263  cfilucfil3  19264  bcthlem1  19269  bcth  19274  ishl2  19316  pmltpclem1  19337  elovolm  19363  ovolgelb  19368  ovolicc  19411  mbfaddlem  19544  i1fres  19589  mbfi1fseqlem4  19602  itg2l  19613  itg2leub  19618  itg2seq  19626  isibl  19649  iblitg  19652  dfitg  19653  itgeq2  19661  itgvallem  19668  iblcnlem1  19671  iblrelem  19674  iblpos  19676  ellimc3  19758  limciun  19773  limcun  19774  dvmptfsum  19851  dveflem  19855  lhop1lem  19889  dvfsumlem2  19903  dvfsumlem4  19905  mpfind  19957  pf1ind  19967  elply2  20107  plypf1  20123  coeval  20134  plydivlem4  20205  sincosq3sgn  20400  vmasum  20992  lgsqrlem1  21117  lgsquadlem1  21130  2sqlem8  21148  2sqlem9  21149  2sqlem11  21151  dchrisumlema  21174  dchrisumlem2  21176  pntibndlem3  21278  pntibnd  21279  pntleme  21294  pntlemp  21296  usgraedg4  21398  cusgrafilem2  21481  cusgrafi  21483  uvtx01vtx  21493  usgrnloop  21555  spthonepeq  21579  usgrcyclnl2  21620  4cycl4v4e  21645  4cycl4dv4e  21647  iseupa  21679  eupath2lem3  21693  isgrpo  21776  isgrp2d  21815  isgrpda  21877  ismndo  21923  drngoi  21987  vci  22019  isvclem  22048  nmoofval  22255  nmooval  22256  nmosetn0  22258  nmoolb  22264  nmoubi  22265  nmoo0  22284  nmlno0lem  22286  isphg  22310  norm3lemt  22646  chlimi  22729  ocsh  22777  cmbr  23078  chscllem2  23132  spansncv  23147  eigorth  23333  nmopval  23351  nmopsetn0  23360  nmfnval  23371  nmfnsetn0  23373  nmoplb  23402  nmfnlb  23419  nmopnegi  23460  nmop0  23481  nmfn0  23482  nmlnop0iALT  23490  nmopun  23509  nmcexi  23521  branmfn  23600  leopmuli  23628  pjnmopi  23643  cvbr  23777  mdbr  23789  dmdbr  23794  atom1d  23848  chrelat2  23865  atcvati  23881  atord  23883  atcvat2  23884  chirredlem4  23888  mdsymlem5  23902  fmptcof2  24068  ofpreima  24073  funcnv4mpt  24077  2ndpreima  24088  xeqlelt  24131  ishashinf  24151  isofld  24227  ofldadd  24230  ofldmul  24231  esumcvg  24468  sitgval  24639  lgamgulmlem2  24806  erdszelem3  24871  erdsze  24880  pconcn  24903  cnpcon  24909  txpcon  24911  conpcon  24914  cvmscbv  24937  iscvm  24938  cvmsi  24944  cvmsval  24945  relexp0  25121  relexpsucr  25122  relexpsucl  25124  relexpadd  25130  relexpindlem  25131  mulle0b  25184  prodfdiv  25216  ntrivcvgn0  25218  ntrivcvgmullem  25221  prodeq1f  25226  prodeq2w  25230  prodeq2ii  25231  prodmo  25254  zprod  25255  fprod  25259  fprodntriv  25260  elima4  25396  dfrdg2  25415  dfrdg3  25416  elpred  25444  trpredrec  25508  poseq  25520  soseq  25521  sltval  25594  nocvxminlem  25637  nofulllem1  25649  elfuns  25752  brimg  25774  brsuccf  25778  dfrdg4  25787  tfrqfree  25788  brcgr  25831  brbtwn2  25836  colinearalg  25841  ax5seg  25869  axcontlem5  25899  axcontlem10  25904  brofs  25931  funtransport  25957  fvtransport  25958  brifs  25969  lineext  26002  brfs  26005  btwnconn1lem11  26023  btwnconn1lem14  26026  brsegle  26034  segletr  26040  segleantisym  26041  seglelin  26042  funray  26066  fvray  26067  funline  26068  fvline  26070  ellines  26078  linethru  26079  mblfinlem2  26235  mblfinlem3  26236  ismblfin  26237  mbfresfi  26243  itg2addnclem  26246  itg2addnclem3  26248  itg2addnc  26249  ftc1anclem7  26276  ftc1anc  26278  areacirclem6  26287  trer  26310  opnrebl2  26315  nn0prpwlem  26316  isfne4  26340  isfne2  26342  isfne3  26343  islocfin  26367  unirep  26405  fnopabeqd  26412  fdc  26440  fdc1  26441  istotbnd  26469  heibor1lem  26509  heibor  26521  isriscg  26591  iscringd  26600  isidlc  26616  prtlem16  26709  prtlem15  26715  ismrcd1  26743  ismrcd2  26744  mzpcompact2lem  26799  eldioph  26807  eldioph2  26811  eldioph2b  26812  eldioph3  26815  diophin  26822  diophun  26823  diophrex  26825  rexrabdioph  26845  fphpd  26868  fphpdo  26869  pellexlem3  26885  monotuz  26995  monotoddzzfi  26996  monotoddzz  26997  oddcomabszz  26998  jm2.27  27070  rmydioph  27076  expdiophlem1  27083  expdiophlem2  27084  aomclem6  27125  aomclem8  27127  islssfg  27136  islssfg2  27137  frlmup1  27218  hbtlem2  27296  hbtlem4  27298  hbtlem5  27300  hbtlem6  27301  dgraaval  27317  flcidc  27347  psgnunilem3  27387  psgneu  27397  psgnvali  27399  psgnvalii  27400  2sbc6g  27583  2sbc5g  27584  iotasbc2  27588  pm14.122a  27590  pm14.123a  27593  fmul01  27677  fmuldfeqlem1  27679  fmuldfeq  27680  fmul01lt1lem1  27681  fmul01lt1lem2  27682  climmulf  27697  climexp  27698  climsuse  27701  climrecf  27702  climinff  27704  stoweidlem3  27719  stoweidlem4  27720  stoweidlem7  27723  stoweidlem15  27731  stoweidlem16  27732  stoweidlem17  27733  stoweidlem19  27735  stoweidlem20  27736  stoweidlem22  27738  stoweidlem23  27739  stoweidlem27  27743  stoweidlem30  27746  stoweidlem32  27748  stoweidlem34  27750  stoweidlem42  27758  stoweidlem43  27759  stoweidlem48  27764  stoweidlem51  27767  stoweidlem59  27775  stoweidlem60  27776  2reu4a  27934  f12dfv  28066  f13dfv  28067  swrdccatin1d  28186  swrdccatin2d  28187  swrdccatin12d  28188  usgra2wlkspthlem1  28259  el2wlkonot  28289  el2spthonot  28290  el2spthonot0  28291  usg2spthonot  28308  usg2spthonot0  28309  usg2spthonot1  28310  1vwmgra  28330  3vfriswmgra  28332  3cyclfrgrarn1  28339  4cycl2vnunb  28344  vdn1frgrav2  28353  vdgn1frgrav2  28354  frgrancvvdeqlemB  28364  usg2spot2nb  28391  usgreg2spot  28393  2spotmdisj  28394  usgreghash2spot  28395  bnj976  29085  bnj852  29229  bnj1014  29268  bnj1015  29269  bnj1118  29290  bnj1123  29292  bnj1148  29302  bnj1171  29306  bnj1373  29336  bnj1489  29362  lsmsat  29743  lsmsatcv  29745  islshpat  29752  lcvfbr  29755  lcvbr  29756  lsatcv0  29766  islshpkrN  29855  cvrval  30004  cvrval2  30009  cvrnbtwn2  30010  cvlexch1  30063  hlsuprexch  30115  cvrval5  30149  cvrat  30156  cvrat42  30178  3dim0  30191  3dim2  30202  islpln3  30267  islpln5  30269  islvol3  30310  islvol5  30313  4atlem11  30343  lineset  30472  isline  30473  ispsubsp2  30480  isline2  30508  isline3  30510  elpaddat  30538  elpadd2at  30540  dalawlem15  30619  pclfinclN  30684  4atex  30810  4atex2  30811  4atex3  30815  ltrnu  30855  cdleme0nex  31024  cdleme31so  31113  cdleme31fv  31124  cdleme31fv2  31127  cdlemefrs29pre00  31129  cdlemefrs29cpre1  31132  cdlemftr3  31299  cdlemb3  31340  cdlemg6d  31355  cdlemg33b  31441  cdlemg33c  31442  cdlemg33e  31444  cdlemk42  31675  dvhopellsm  31852  dibelval3  31882  diblsmopel  31906  diclspsn  31929  dihval  31967  dihopelvalcpre  31983  dih1dimatlem  32064  dihglb2  32077  dochkrshp3  32123  dihjatcclem4  32156  dihjat1lem  32163  mapdval  32363  mapdpglem30  32437
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