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

Theorem anbi1i 676
Description: Introduce a right 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
bi.aa  |-  ( ph  <->  ps )
Assertion
Ref Expression
anbi1i  |-  ( (
ph  /\  ch )  <->  ( ps  /\  ch )
)

Proof of Theorem anbi1i
StepHypRef Expression
1 bi.aa . . 3  |-  ( ph  <->  ps )
21a1i 10 . 2  |-  ( ch 
->  ( ph  <->  ps )
)
32pm5.32ri 619 1  |-  ( (
ph  /\  ch )  <->  ( ps  /\  ch )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358
This theorem is referenced by:  anbi2ci  677  anbi12i  678  pm5.53  771  an12  772  anandi  801  pm5.75  903  3ancoma  941  3ioran  950  an6  1261  19.26-3an  1585  19.28  1818  eeeanv  1867  sb3an  2023  pm11.07  2067  2eu6  2241  r19.26-3  2690  r19.41  2705  rexcomf  2712  3reeanv  2721  cbvreu  2775  ceqsex3v  2839  rexab  2941  rexrab  2942  rmo4  2971  reuind  2981  rmo3  3091  ssrab  3264  rexun  3368  elin3  3373  inass  3392  dfun2  3417  indifdir  3438  difin2  3443  inrab2  3454  rabun2  3460  reuun2  3464  undif4  3524  difin0ss  3533  rexsns  3684  rexdifsn  3766  2ralunsn  3832  iuncom4  3928  iunxiun  4000  disjxun  4037  zfrep4  4155  inuni  4189  otth2  4265  copsexg  4268  copsex4g  4271  opeqsn  4278  opelopabsbOLD  4289  dfid3  4326  wefrc  4403  reusv2lem4  4554  reusv2  4556  rabxp  4741  opeliunxp  4756  xpundir  4758  xpiundi  4759  xpiundir  4760  brinxp2  4767  brres  4977  brresg  4979  dmres  4992  resiexg  5013  dminss  5111  imainss  5112  ssrnres  5132  elxp4  5176  elxp5  5177  cnvresima  5178  coundi  5190  resco  5193  imaco  5194  coiun  5198  coi1  5204  coass  5207  cnvpo  5229  dffun2  5281  fncnv  5330  imadif  5343  mptun  5390  fcnvres  5434  dff1o2  5493  dff1o3  5494  ffoss  5521  f11o  5522  brprcneu  5534  fvun2  5607  eqfnfv3  5640  respreima  5670  f1ompt  5698  fsn  5712  abrexco  5782  opabex3  5785  imaiun  5787  abexssex  5797  f1mpt  5801  dff1o6  5807  oprabid  5898  dfoprab2  5911  oprab4  5933  mpt2mptx  5954  elxp7  6168  difxp  6169  dfopab2  6190  dfoprab3s  6191  copsex2gb  6196  1stconst  6223  2ndconst  6224  frxp  6241  xporderlem  6242  brtpos2  6256  tpostpos  6270  tposmpt2  6287  oarec  6576  oeeui  6616  oeeu  6617  ovec  6784  map0e  6821  mapsncnv  6830  dfixp  6835  domen  6891  mapsnen  6954  xpsnen  6962  xpcomco  6968  xpassen  6972  sbthlem9  6995  frfi  7118  marypha2lem2  7205  epfrs  7429  tcsni  7444  cp  7577  bnd2  7579  dfac5lem1  7766  dfac5lem2  7767  dfac5lem5  7770  kmlem3  7794  dfackm  7808  cfval2  7902  cflim3  7904  cfss  7907  cfslb  7908  zfcndrep  8252  eltsk2g  8389  ltexpi  8542  recmulnq  8604  ltexprlem4  8679  addcnsr  8773  mulcnsr  8774  ltresr  8778  axrrecex  8801  elnnz  10050  elnn0z  10052  fnn0ind  10127  rexuz2  10286  rexrp  10389  elixx3g  10685  elfz2  10805  elfzuzb  10808  elfz2nn0  10837  fznn0  10867  fznn  10868  elfzo2  10894  fzind2  10939  hashf1lem1  11409  hashf1lem2  11410  fz1isolem  11415  fsum2dlem  12249  sinltx  12485  divalglem10  12617  divalgb  12619  isprm2  12782  infpn2  12976  prdsle  13377  prdsless  13378  prdsleval  13392  imasleval  13459  oppcsect  13692  elhoma  13880  ispos2  14098  tosso  14158  ismhm  14433  issubm  14441  submacs  14458  issubg  14637  issubg3  14653  gaorb  14777  efgcpbllema  15079  efgcpbllemb  15080  frgpuplem  15097  subgdmdprd  15285  dprd2d2  15295  dfrhm2  15514  drngprop  15539  drngid2  15544  opprdrng  15552  issubrg  15561  isabv  15600  islss  15708  islbs  15845  lsmspsn  15853  isassa  16072  aspval2  16102  ltbval  16229  opsrle  16233  opsrtoslem1  16241  isobs  16636  istps2OLD  16675  istps3OLD  16676  istps5OLD  16678  ntreq0  16830  restntr  16928  cnrest  17029  hausnei2  17097  cmpcov2  17133  cmpsub  17143  uncmp  17146  cmpfi  17151  llyi  17216  subislly  17223  iskgen3  17260  1stckgenlem  17264  ptpjpre1  17282  txcnpi  17318  txtube  17350  hausdiag  17355  txlm  17358  txkgen  17362  cfinfil  17604  csdfil  17605  supfil  17606  fin1aufil  17643  elflim2  17675  hauspwpwf1  17698  txflf  17717  isfcls  17720  alexsubALTlem3  17759  alexsubALT  17761  istmd  17773  istgp  17776  tgphaus  17815  divstgplem  17819  istrg  17862  istdrg  17864  istlm  17883  blres  17993  isms2  18012  metrest  18086  isngp  18134  isnlm  18202  elii1  18449  iscph  18622  isbn  18776  limcrcl  19240  ig1pval3  19576  plydivex  19693  ellogdm  20002  cubic  20161  dmarea  20268  vmasum  20471  lgsquadlem1  20609  lgsquadlem2  20610  avril1  20852  islno  21347  h2hlm  21576  hcau  21779  hhsssh2  21863  dfch2  22002  elcnop  22453  ellnop  22454  elhmop  22469  elcnfn  22478  ellnfn  22479  dmadjss  22483  adjeu  22485  adjval  22486  hhcno  22500  hhcnf  22501  eleigvec  22553  isst  22809  ishst  22810  cvnbtwn3  22884  cvnbtwn4  22885  chirredi  22990  sumdmdii  23011  ballotlemelo  23062  ballotlem2  23063  ballotlemfc0  23067  ballotlemfcc  23068  or3di  23139  rexunirn  23156  rmo3f  23194  rmo4fOLD  23195  sigaex  23485  sigaval  23486  isrnsigaOLD  23488  probun  23637  erdszelem1  23737  iscvm  23805  vdgrun  23908  dfso3  24089  coepr  24180  dfpo2  24183  dfdm5  24203  dfrn5  24204  preduz  24271  wfi  24278  frind  24314  soseq  24325  wfrlem11  24337  tfrALTlem  24347  frrlem5c  24358  elno3  24380  nofulllem5  24431  brtxp  24491  brpprod  24496  dfon3  24503  dffun10  24524  elfuns  24525  brimg  24547  brapply  24548  brcup  24549  brcap  24550  brsuccf  24551  funpartlem  24552  funpartfun  24553  brrestrict  24559  dfrdg4  24560  tfrqfree  24561  colinearalg  24610  axeuclid  24663  axcontlem2  24665  axcontlem5  24668  lineunray  24842  ellines  24847  rabiun2  24997  ovoliunnfl  25001  itg2addnclem2  25004  itg2addnc  25005  fates  25058  eqvinopb  25068  elo  25144  restidsing  25179  dff1o6f  25195  isidlNEW  25549  vecax3  25558  sallnei  25632  fgsb2  25658  isfunb  25938  cnvresimaOLD  26329  finminlem  26334  fneval  26390  neibastop3  26414  isbnd2  26610  bndss  26613  heibor1lem  26636  heibor1  26637  isrngohom  26699  isidl  26742  prtlem70  26818  prtlem100  26824  prter2  26852  elmzpcl  26907  mzpindd  26927  fphpd  27002  pw2f1ocnv  27233  islmodfg  27270  islssfg2  27272  islinds  27382  isdomn3  27626  pm13.192  27713  opabex3d  28190  4fvwrd4  28220  s4f1o  28225  nb3graprlem2  28288  nb3grapr  28289  nb3grapr2  28290  nb3gra2nb  28291  cusgra2v  28297  trls  28335  3v3e3cycl2  28410  2pthfrgrarn  28433  opelopab4  28616  a9e2nd  28623  en3lplem2VD  28936  a9e2ndVD  29000  a9e2ndALT  29023  bnj248  29041  bnj250  29042  bnj268  29050  bnj312  29053  bnj945  29121  bnj110  29206  bnj849  29273  bnj882  29274  bnj893  29276  bnj916  29281  bnj983  29299  bnj1040  29318  bnj1175  29350  sb3anNEW7  29611  eeeanvOLD7  29658  pm11.07OLD7  29716  equvinv  29736  lsateln0  29807  islshpat  29829  lcvnbtwn3  29840  islfl  29872  ishlat1  30164  ishlat2  30165  cvrat4  30254  islvol5  30390  psubspset  30555  snatpsubN  30561  dalawlem13  30694  psubclsetN  30747  isltrn2N  30931  cdlemftr3  31376  dibelval3  31959  dicval2  31991  dicopelval2  31993  dicelval2N  31994  dihglb2  32154  islpolN  32295  lcfls1c  32348  mapdvalc  32441  mapdval4N  32444  mapdordlem1a  32446
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 177  df-an 360
  Copyright terms: Public domain W3C validator