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  1582  19.28  1806  eeeanv  1855  sb3an  2010  pm11.07  2054  2eu6  2228  r19.26-3  2677  r19.41  2692  rexcomf  2699  3reeanv  2708  cbvreu  2762  ceqsex3v  2826  rexab  2928  rexrab  2929  rmo4  2958  reuind  2968  rmo3  3078  ssrab  3251  rexun  3355  elin3  3360  inass  3379  dfun2  3404  indifdir  3425  difin2  3430  inrab2  3441  rabun2  3447  reuun2  3451  undif4  3511  difin0ss  3520  rexsns  3671  rexdifsn  3753  2ralunsn  3816  iuncom4  3912  iunxiun  3984  disjxun  4021  zfrep4  4139  inuni  4173  otth2  4249  copsexg  4252  copsex4g  4255  opeqsn  4262  opelopabsbOLD  4273  dfid3  4310  wefrc  4387  reusv2lem4  4538  reusv2  4540  rabxp  4725  opeliunxp  4740  xpundir  4742  xpiundi  4743  xpiundir  4744  brinxp2  4751  brres  4961  brresg  4963  dmres  4976  resiexg  4997  dminss  5095  imainss  5096  ssrnres  5116  elxp4  5160  elxp5  5161  cnvresima  5162  coundi  5174  resco  5177  imaco  5178  coiun  5182  coi1  5188  coass  5191  cnvpo  5213  dffun2  5265  fncnv  5314  imadif  5327  mptun  5374  fcnvres  5418  dff1o2  5477  dff1o3  5478  ffoss  5505  f11o  5506  brprcneu  5518  fvun2  5591  eqfnfv3  5624  respreima  5654  f1ompt  5682  fsn  5696  abrexco  5766  opabex3  5769  imaiun  5771  abexssex  5781  f1mpt  5785  dff1o6  5791  oprabid  5882  dfoprab2  5895  oprab4  5917  mpt2mptx  5938  elxp7  6152  difxp  6153  dfopab2  6174  dfoprab3s  6175  copsex2gb  6180  1stconst  6207  2ndconst  6208  frxp  6225  xporderlem  6226  brtpos2  6240  tpostpos  6254  tposmpt2  6271  oarec  6560  oeeui  6600  oeeu  6601  ovec  6768  map0e  6805  mapsncnv  6814  dfixp  6819  domen  6875  mapsnen  6938  xpsnen  6946  xpcomco  6952  xpassen  6956  sbthlem9  6979  frfi  7102  marypha2lem2  7189  epfrs  7413  tcsni  7428  cp  7561  bnd2  7563  dfac5lem1  7750  dfac5lem2  7751  dfac5lem5  7754  kmlem3  7778  dfackm  7792  cfval2  7886  cflim3  7888  cfss  7891  cfslb  7892  zfcndrep  8236  eltsk2g  8373  ltexpi  8526  recmulnq  8588  ltexprlem4  8663  addcnsr  8757  mulcnsr  8758  ltresr  8762  axrrecex  8785  elnnz  10034  elnn0z  10036  fnn0ind  10111  rexuz2  10270  rexrp  10373  elixx3g  10669  elfz2  10789  elfzuzb  10792  elfz2nn0  10821  fznn0  10851  fznn  10852  elfzo2  10878  fzind2  10923  hashf1lem1  11393  hashf1lem2  11394  fz1isolem  11399  fsum2dlem  12233  sinltx  12469  divalglem10  12601  divalgb  12603  isprm2  12766  infpn2  12960  prdsle  13361  prdsless  13362  prdsleval  13376  imasleval  13443  oppcsect  13676  elhoma  13864  ispos2  14082  tosso  14142  ismhm  14417  issubm  14425  submacs  14442  issubg  14621  issubg3  14637  gaorb  14761  efgcpbllema  15063  efgcpbllemb  15064  frgpuplem  15081  subgdmdprd  15269  dprd2d2  15279  dfrhm2  15498  drngprop  15523  drngid2  15528  opprdrng  15536  issubrg  15545  isabv  15584  islss  15692  islbs  15829  lsmspsn  15837  isassa  16056  aspval2  16086  ltbval  16213  opsrle  16217  opsrtoslem1  16225  isobs  16620  istps2OLD  16659  istps3OLD  16660  istps5OLD  16662  ntreq0  16814  restntr  16912  cnrest  17013  hausnei2  17081  cmpcov2  17117  cmpsub  17127  uncmp  17130  cmpfi  17135  llyi  17200  subislly  17207  iskgen3  17244  1stckgenlem  17248  ptpjpre1  17266  txcnpi  17302  txtube  17334  hausdiag  17339  txlm  17342  txkgen  17346  cfinfil  17588  csdfil  17589  supfil  17590  fin1aufil  17627  elflim2  17659  hauspwpwf1  17682  txflf  17701  isfcls  17704  alexsubALTlem3  17743  alexsubALT  17745  istmd  17757  istgp  17760  tgphaus  17799  divstgplem  17803  istrg  17846  istdrg  17848  istlm  17867  blres  17977  isms2  17996  metrest  18070  isngp  18118  isnlm  18186  elii1  18433  iscph  18606  isbn  18760  limcrcl  19224  ig1pval3  19560  plydivex  19677  ellogdm  19986  cubic  20145  dmarea  20252  vmasum  20455  lgsquadlem1  20593  lgsquadlem2  20594  avril1  20836  islno  21331  h2hlm  21560  hcau  21763  hhsssh2  21847  dfch2  21986  elcnop  22437  ellnop  22438  elhmop  22453  elcnfn  22462  ellnfn  22463  dmadjss  22467  adjeu  22469  adjval  22470  hhcno  22484  hhcnf  22485  eleigvec  22537  isst  22793  ishst  22794  cvnbtwn3  22868  cvnbtwn4  22869  chirredi  22974  sumdmdii  22995  ballotlemelo  23046  ballotlem2  23047  ballotlemfc0  23051  ballotlemfcc  23052  or3di  23123  rexunirn  23140  rmo3f  23178  rmo4fOLD  23179  sigaex  23470  sigaval  23471  isrnsigaOLD  23473  probun  23622  erdszelem1  23722  iscvm  23790  vdgrun  23893  dfso3  24074  coepr  24109  dfpo2  24112  dfdm5  24132  dfrn5  24133  preduz  24200  wfi  24207  frind  24243  soseq  24254  wfrlem11  24266  tfrALTlem  24276  frrlem5c  24287  elno3  24309  nofulllem5  24360  brtxp  24420  brpprod  24425  dfon3  24432  dffun10  24453  elfuns  24454  brimg  24476  brapply  24477  brcup  24478  brcap  24479  brsuccf  24480  brrestrict  24487  dfrdg4  24488  tfrqfree  24489  colinearalg  24538  axeuclid  24591  axcontlem2  24593  axcontlem5  24596  lineunray  24770  ellines  24775  fates  24955  eqvinopb  24965  elo  25041  restidsing  25076  dff1o6f  25092  isidlNEW  25446  vecax3  25455  sallnei  25529  fgsb2  25555  isfunb  25835  cnvresimaOLD  26226  finminlem  26231  fneval  26287  neibastop3  26311  isbnd2  26507  bndss  26510  heibor1lem  26533  heibor1  26534  isrngohom  26596  isidl  26639  prtlem70  26715  prtlem100  26721  prter2  26749  elmzpcl  26804  mzpindd  26824  fphpd  26899  pw2f1ocnv  27130  islmodfg  27167  islssfg2  27169  islinds  27279  isdomn3  27523  pm13.192  27610  s4f1o  28093  cusgra2v  28158  opelopab4  28317  a9e2nd  28324  en3lplem2VD  28620  a9e2ndVD  28684  a9e2ndALT  28707  bnj248  28725  bnj250  28726  bnj268  28734  bnj312  28737  bnj945  28805  bnj110  28890  bnj849  28957  bnj882  28958  bnj893  28960  bnj916  28965  bnj983  28983  bnj1040  29002  bnj1175  29034  equvinv  29114  lsateln0  29185  islshpat  29207  lcvnbtwn3  29218  islfl  29250  ishlat1  29542  ishlat2  29543  cvrat4  29632  islvol5  29768  psubspset  29933  snatpsubN  29939  dalawlem13  30072  psubclsetN  30125  isltrn2N  30309  cdlemftr3  30754  dibelval3  31337  dicval2  31369  dicopelval2  31371  dicelval2N  31372  dihglb2  31532  islpolN  31673  lcfls1c  31726  mapdvalc  31819  mapdval4N  31822  mapdordlem1a  31824
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