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

Theorem anbi2d 686
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 24 . 2  |-  ( ph  ->  ( th  ->  ( ps 
<->  ch ) ) )
32pm5.32d 622 1  |-  ( ph  ->  ( ( th  /\  ps )  <->  ( th  /\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360
This theorem is referenced by:  anbi2  690  anbi12d  693  bi2anan9  845  sbrim  2141  2eu6  2373  eleq2  2504  ceqsex2  3001  ceqsex6v  3005  vtocl2gaf  3027  ceqsrex2v  3080  moeq3  3120  mob2  3123  eqreu  3135  nelrdva  3152  undif4  3712  r19.27z  3754  r19.27zv  3755  ssunsn2  3987  preq12bg  4006  opeq2  4014  ralunsn  4032  intab  4109  disjxun  4241  opabbid  4301  opthg  4471  pocl  4545  isso2i  4570  ordelord  4638  ordtri4  4653  dfwe2  4797  dflim4  4863  tfisi  4873  xpeq2  4928  rabxp  4949  vtoclr  4957  opeliunxp  4964  posn  4981  opbrop  4990  elrnmpt1  5154  dfres2  5228  brcodir  5288  poltletr  5304  xp11  5339  elxp4  5392  elxp5  5393  fununi  5552  fneq2  5570  fnun  5586  feq3  5613  foeq3  5686  funbrfv  5801  ssimaexg  5825  fvopab3g  5838  fvopab3ig  5839  fvelrn  5902  fmptco  5937  elunirnALT  6036  isoeq2  6076  isoeq3  6077  isoini  6094  isopolem  6101  f1oiso  6107  f1oiso2  6108  oprabbid  6163  cbvoprab3  6184  mpt2mptx  6200  mpt2fun  6208  ov  6229  ov3  6246  ov6g  6247  ovg  6248  caoftrn  6375  f1o2ndf1  6490  frxp  6492  xporderlem  6493  fnwelem  6497  brtpos2  6521  dftpos4  6534  riotabidv  6587  onfununi  6639  recseq  6670  tfrlem1  6672  omopth  6937  brecop  7033  eroveu  7035  erovlem  7036  erov  7037  ecopovtrn  7043  th3qlem1  7046  th3qlem2  7047  th3q  7049  elpmg  7068  ixpsnf1o  7138  domeng  7158  dom2lem  7183  xpcomco  7234  xpassen  7238  xpdom2  7239  omxpenlem  7245  xpf1o  7305  unxpdom  7352  isinf  7358  findcard2  7384  fiint  7419  supeq2  7489  inf0  7612  scott0  7848  isinffi  7917  isacn  7963  aceq1  8036  aceq0  8037  aceq2  8038  dfac3  8040  dfac5lem1  8042  dfac2  8049  dfac12lem2  8062  kmlem8  8075  kmlem14  8081  infmap2  8136  cfval  8165  cflim3  8180  sornom  8195  infpssrlem4  8224  isf32lem9  8279  domtriomlem  8360  axdc2lem  8366  zfac  8378  ac6num  8397  axrepndlem1  8505  axunndlem1  8508  axregnd  8517  axinfndlem1  8518  axacndlem4  8523  axacndlem5  8524  zfcndac  8532  fpwwe2lem5  8547  pwfseqlem4a  8574  pwfseqlem4  8575  alephgch  8587  wunex2  8651  tskord  8693  nqereu  8844  ordpipq  8857  prcdnq  8908  prnmax  8910  genpnnp  8920  distrlem5pr  8942  ltprord  8945  ltexprlem3  8953  ltexprlem4  8954  ltexpri  8958  prlem936  8962  reclem2pr  8963  ltsosr  9007  mulgt0sr  9018  ltresr  9053  axpre-lttrn  9079  axpre-mulgt0  9081  eqlelt  9200  lesub0  9582  wloglei  9597  sup3  10003  infm3  10005  prime  10388  fzind  10406  uzwo  10577  uzwoOLD  10578  zbtwnre  10610  xltnegi  10840  xmulneg1  10886  ixxval  10962  fzval  11083  elfzm11  11154  elfzo  11180  seqof2  11419  nn0opth2  11603  facwordi  11618  hashnn0n0nn  11702  brfi1uzind  11753  shftfval  11923  shftfib  11925  shftfn  11926  2shfti  11933  abs1m  12177  cau3lem  12196  caubnd2  12199  clim  12326  rlim  12327  clim2  12336  climi  12342  o1lo1  12369  rlimcn2  12422  climcn2  12424  addcn2  12425  subcn2  12426  mulcn2  12427  o1of2  12444  isercoll  12499  caurcvg2  12509  sumeq2w  12524  sumeq2ii  12525  cbvsum  12527  summo  12549  fsum  12552  sinbnd  12819  cosbnd  12820  divalgb  12962  ndvdssub  12965  smupp1  13030  smueqlem  13040  gcdval  13046  gcdcllem2  13050  gcdneg  13064  gcdass  13083  algcvgblem  13106  prmind2  13128  qredeq  13144  euclemma  13146  qnumval  13167  qdenval  13168  eulerthlem2  13209  pceu  13258  pczpre  13259  pcdiv  13264  prmpwdvds  13310  prmreclem5  13326  vdwapun  13380  ramub2  13420  rami  13421  ramcl  13435  ismred2  13866  isacs  13914  iscatd2  13944  catpropd  13973  oppccatid  13983  isinv  14023  isssc  14058  funcres2b  14132  funcpropd  14135  fucinv  14208  yoniso  14420  prslem  14426  drsdir  14430  drsdirfi  14433  posi  14445  isposd  14450  pltval  14455  plttr  14465  isipodrs  14625  ipodrsima  14629  spwval  14695  dirge  14720  mndlem1  14732  gsumpropd  14814  gsumress  14815  divsgrp2  14974  resscntz  15168  isslw  15280  subgslw  15288  iscmnd  15462  gsumval3eu  15551  gsumval3  15552  dmdprd  15597  subgdmdprd  15630  dprd2d2  15640  pgpfac1  15676  pgpfaclem2  15678  pgpfaclem3  15679  pgpfac  15680  ablfaclem1  15681  divsrng2  15764  dvdsrval  15788  crngunit  15805  dfrhm2  15859  isdrngd  15898  abvpropd  15968  islmod  15992  lssacs  16081  lsspropd  16131  islmhm  16141  lbspropd  16209  fiidomfld  16406  ltbval  16570  opsrval  16573  pjfval2  16974  eltopspOLD  17021  istpsOLD  17023  basis2  17054  eltg2  17061  isclo  17189  isnei  17205  isneip  17207  neiptopnei  17234  restbas  17260  restcld  17274  neitr  17282  iscnp  17339  iscnp3  17346  tgcn  17354  cnpimaex  17358  lmbrf  17362  cncnp  17382  cnprest2  17392  isreg  17434  regsep  17436  isnrm  17437  ist1-2  17449  nrmsep3  17457  isnrm2  17460  hauscmplem  17507  dfcon2  17520  is1stc  17542  1stcclb  17545  1stcfb  17546  is2ndc  17547  2ndc1stc  17552  1stcrest  17554  2ndcsep  17560  1stccnp  17563  islly  17569  llyeq  17571  llyi  17575  hausllycmp  17595  lly1stc  17597  txbas  17637  ptpjpre1  17641  elpt  17642  txcnpi  17678  ptpjopn  17682  ptcldmpt  17684  ptclsg  17685  txcnp  17690  ptcnp  17692  hausdiag  17715  tx1stc  17720  xkoinjcn  17757  imasnopn  17760  imasncld  17761  imasncls  17762  fbfinnfr  17911  snfil  17934  uffix2  17994  elfm  18017  elfm2  18018  fmco  18031  hauspwpwf1  18057  flfnei  18061  isflf  18063  lmflf  18075  fclscf  18095  isfcf  18104  alexsublem  18113  cnextcn  18136  cnextfres  18137  eltsms  18200  tsmsres  18211  tsmsf1o  18212  ustuqtop4  18312  ispsmet  18373  ismet  18391  isxmet  18392  ismet2  18401  imasdsf1olem  18441  blres  18499  met2ndc  18591  metcnp3  18608  nrmmetd  18660  pi1grplem  19112  lmmbr2  19250  lmmbrf  19253  iscau2  19268  iscau4  19270  caucfil  19274  lmclim  19293  cfilucfil3OLD  19309  cfilucfil3  19310  bcthlem1  19315  bcth  19320  ishl2  19362  pmltpclem1  19383  elovolm  19409  ovolgelb  19414  ovolicc  19457  mbfaddlem  19588  i1fres  19633  mbfi1fseqlem4  19646  itg2l  19657  itg2leub  19662  itg2seq  19670  isibl  19693  iblitg  19696  dfitg  19697  itgeq2  19705  itgvallem  19712  iblcnlem1  19715  iblrelem  19718  iblpos  19720  ellimc3  19804  limciun  19819  limcun  19820  dvmptfsum  19897  dveflem  19901  lhop1lem  19935  dvfsumlem2  19949  dvfsumlem4  19951  mpfind  20003  pf1ind  20013  elply2  20153  plypf1  20169  coeval  20180  plydivlem4  20251  sincosq3sgn  20446  vmasum  21038  lgsqrlem1  21163  lgsquadlem1  21176  2sqlem8  21194  2sqlem9  21195  2sqlem11  21197  dchrisumlema  21220  dchrisumlem2  21222  pntibndlem3  21324  pntibnd  21325  pntleme  21340  pntlemp  21342  usgraedg4  21444  cusgrafilem2  21527  cusgrafi  21529  uvtx01vtx  21539  usgrnloop  21601  spthonepeq  21625  usgrcyclnl2  21666  4cycl4v4e  21691  4cycl4dv4e  21693  iseupa  21725  eupath2lem3  21739  isgrpo  21822  isgrp2d  21861  isgrpda  21923  ismndo  21969  drngoi  22033  vci  22065  isvclem  22094  nmoofval  22301  nmooval  22302  nmosetn0  22304  nmoolb  22310  nmoubi  22311  nmoo0  22330  nmlno0lem  22332  isphg  22356  norm3lemt  22692  chlimi  22775  ocsh  22823  cmbr  23124  chscllem2  23178  spansncv  23193  eigorth  23379  nmopval  23397  nmopsetn0  23406  nmfnval  23417  nmfnsetn0  23419  nmoplb  23448  nmfnlb  23465  nmopnegi  23506  nmop0  23527  nmfn0  23528  nmlnop0iALT  23536  nmopun  23555  nmcexi  23567  branmfn  23646  leopmuli  23674  pjnmopi  23689  cvbr  23823  mdbr  23835  dmdbr  23840  atom1d  23894  chrelat2  23911  atcvati  23927  atord  23929  atcvat2  23930  chirredlem4  23934  mdsymlem5  23948  fmptcof2  24111  ofpreima  24116  funcnv4mpt  24120  2ndpreima  24131  xeqlelt  24174  ishashinf  24194  isofld  24270  ofldadd  24273  ofldmul  24274  esumcvg  24511  sitgval  24682  lgamgulmlem2  24849  erdszelem3  24914  erdsze  24923  pconcn  24946  cnpcon  24952  txpcon  24954  conpcon  24957  cvmscbv  24980  iscvm  24981  cvmsi  24987  cvmsval  24988  relexp0  25164  relexpsucr  25165  relexpsucl  25167  relexpadd  25173  relexpindlem  25174  mulle0b  25227  prodfdiv  25259  ntrivcvgn0  25261  ntrivcvgmullem  25264  prodeq1f  25269  prodeq2w  25273  prodeq2ii  25274  prodmo  25297  zprod  25298  fprod  25302  fprodntriv  25303  elima4  25439  dfrdg2  25458  dfrdg3  25459  elpred  25487  trpredrec  25551  poseq  25563  soseq  25564  sltval  25637  nocvxminlem  25680  nofulllem1  25692  elfuns  25795  brimg  25817  brsuccf  25821  dfrdg4  25830  tfrqfree  25831  brcgr  25874  brbtwn2  25879  colinearalg  25884  ax5seg  25912  axcontlem5  25942  axcontlem10  25947  brofs  25974  funtransport  26000  fvtransport  26001  brifs  26012  lineext  26045  brfs  26048  btwnconn1lem11  26066  btwnconn1lem14  26069  brsegle  26077  segletr  26083  segleantisym  26084  seglelin  26085  funray  26109  fvray  26110  funline  26111  fvline  26113  ellines  26121  linethru  26122  mblfinlem3  26285  mblfinlem4  26286  ismblfin  26287  mbfresfi  26293  itg2addnclem  26298  itg2addnclem3  26300  itg2addnc  26301  ftc1anclem7  26328  ftc1anc  26330  areacirclem5  26338  trer  26361  opnrebl2  26366  nn0prpwlem  26367  isfne4  26391  isfne2  26393  isfne3  26394  islocfin  26418  unirep  26456  fnopabeqd  26463  fdc  26491  fdc1  26492  istotbnd  26520  heibor1lem  26560  heibor  26572  isriscg  26642  iscringd  26651  isidlc  26667  prtlem16  26830  prtlem15  26836  ismrcd1  26864  ismrcd2  26865  mzpcompact2lem  26920  eldioph  26928  eldioph2  26932  eldioph2b  26933  eldioph3  26936  diophin  26943  diophun  26944  diophrex  26946  rexrabdioph  26966  fphpd  26989  fphpdo  26990  pellexlem3  27006  monotuz  27116  monotoddzzfi  27117  monotoddzz  27118  oddcomabszz  27119  jm2.27  27191  rmydioph  27197  expdiophlem1  27204  expdiophlem2  27205  aomclem6  27246  aomclem8  27248  islssfg  27257  islssfg2  27258  frlmup1  27339  hbtlem2  27417  hbtlem4  27419  hbtlem5  27421  hbtlem6  27422  dgraaval  27438  flcidc  27468  psgnunilem3  27508  psgneu  27518  psgnvali  27520  psgnvalii  27521  2sbc6g  27704  2sbc5g  27705  iotasbc2  27709  pm14.122a  27711  pm14.123a  27714  fmul01  27798  fmuldfeqlem1  27800  fmuldfeq  27801  fmul01lt1lem1  27802  fmul01lt1lem2  27803  climmulf  27818  climexp  27819  climsuse  27822  climrecf  27823  climinff  27825  stoweidlem3  27840  stoweidlem4  27841  stoweidlem7  27844  stoweidlem15  27852  stoweidlem16  27853  stoweidlem17  27854  stoweidlem19  27856  stoweidlem20  27857  stoweidlem22  27859  stoweidlem23  27860  stoweidlem27  27864  stoweidlem30  27867  stoweidlem32  27869  stoweidlem34  27871  stoweidlem42  27879  stoweidlem43  27880  stoweidlem48  27885  stoweidlem51  27888  stoweidlem59  27896  stoweidlem60  27897  2reu4a  28055  f12dfv  28196  f13dfv  28197  oprabv  28201  swrdccatin1d  28352  swrdccatin2d  28353  swrdccatin12d  28354  usgra2wlkspthlem1  28442  wwlk  28461  wlklniswwlkn2  28480  el2wlkonot  28499  el2spthonot  28500  el2spthonot0  28501  usg2spthonot  28518  usg2spthonot0  28519  usg2spthonot1  28520  isrusgra  28540  1vwmgra  28565  3vfriswmgra  28567  3cyclfrgrarn1  28574  4cycl2vnunb  28579  vdn1frgrav2  28588  vdgn1frgrav2  28589  frgrancvvdeqlemB  28599  usg2spot2nb  28626  usgreg2spot  28628  2spotmdisj  28629  usgreghash2spot  28630  bnj976  29322  bnj852  29466  bnj1014  29505  bnj1015  29506  bnj1118  29527  bnj1123  29529  bnj1148  29539  bnj1171  29543  bnj1373  29573  bnj1489  29599  lsmsat  29980  lsmsatcv  29982  islshpat  29989  lcvfbr  29992  lcvbr  29993  lsatcv0  30003  islshpkrN  30092  cvrval  30241  cvrval2  30246  cvrnbtwn2  30247  cvlexch1  30300  hlsuprexch  30352  cvrval5  30386  cvrat  30393  cvrat42  30415  3dim0  30428  3dim2  30439  islpln3  30504  islpln5  30506  islvol3  30547  islvol5  30550  4atlem11  30580  lineset  30709  isline  30710  ispsubsp2  30717  isline2  30745  isline3  30747  elpaddat  30775  elpadd2at  30777  dalawlem15  30856  pclfinclN  30921  4atex  31047  4atex2  31048  4atex3  31052  ltrnu  31092  cdleme0nex  31261  cdleme31so  31350  cdleme31fv  31361  cdleme31fv2  31364  cdlemefrs29pre00  31366  cdlemefrs29cpre1  31369  cdlemftr3  31536  cdlemb3  31577  cdlemg6d  31592  cdlemg33b  31678  cdlemg33c  31679  cdlemg33e  31681  cdlemk42  31912  dvhopellsm  32089  dibelval3  32119  diblsmopel  32143  diclspsn  32166  dihval  32204  dihopelvalcpre  32220  dih1dimatlem  32301  dihglb2  32314  dochkrshp3  32360  dihjatcclem4  32393  dihjat1lem  32400  mapdval  32600  mapdpglem30  32674
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 179  df-an 362
  Copyright terms: Public domain W3C validator