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

Theorem anbi1i 677
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 11 . 2  |-  ( ch 
->  ( ph  <->  ps )
)
32pm5.32ri 620 1  |-  ( (
ph  /\  ch )  <->  ( ps  /\  ch )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359
This theorem is referenced by:  anbi2ci  678  anbi12i  679  pm5.53  772  an12  773  anandi  802  pm5.75  904  3ancoma  943  3ioran  952  an6  1263  19.26-3an  1602  19.28  1838  eeeanv  1934  eeeanvOLD  1935  sb3an  2119  pm11.07OLD  2165  2eu6  2339  r19.26-3  2800  r19.41  2820  rexcomf  2827  3reeanv  2836  cbvreu  2890  ceqsex3v  2954  rexab  3057  rexrab  3058  rmo4  3087  reuind  3097  rmo3  3208  ssrab  3381  rexun  3487  elin3  3492  inass  3511  dfun2  3536  indifdir  3557  difin2  3563  inrab2  3574  rabun2  3580  reuun2  3584  undif4  3644  difin0ss  3654  rexsns  3805  rexdifsn  3891  2ralunsn  3964  iuncom4  4060  iunxiun  4133  disjxun  4170  zfrep4  4288  inuni  4322  otth2  4399  copsexg  4402  copsex4g  4405  opeqsn  4412  opelopabsbOLD  4423  dfid3  4459  wefrc  4536  reusv2lem4  4686  reusv2  4688  rabxp  4873  opeliunxp  4888  xpundir  4890  xpiundi  4891  xpiundir  4892  brinxp2  4898  brres  5111  brresg  5113  dmres  5126  resiexg  5147  dminss  5245  imainss  5246  ssrnres  5268  elxp4  5316  elxp5  5317  cnvresima  5318  coundi  5330  resco  5333  imaco  5334  coiun  5338  coi1  5344  coass  5347  cnvpo  5369  xpco  5373  dffun2  5423  fncnv  5474  imadif  5487  mptun  5534  fcnvres  5579  dff1o2  5638  dff1o3  5639  ffoss  5666  f11o  5667  brprcneu  5680  fvun2  5754  eqfnfv3  5788  respreima  5818  f1ompt  5850  fsn  5865  abrexco  5945  opabex3d  5948  opabex3  5949  imaiun  5951  abexssex  5961  f1mpt  5966  dff1o6  5972  oprabid  6064  dfoprab2  6080  oprab4  6102  mpt2mptx  6123  elxp7  6338  difxp  6339  dfopab2  6360  dfoprab3s  6361  copsex2gb  6366  1stconst  6394  2ndconst  6395  frxp  6415  xporderlem  6416  brtpos2  6444  tpostpos  6458  tposmpt2  6475  oarec  6764  oeeui  6804  oeeu  6805  ovec  6973  map0e  7010  mapsncnv  7019  dfixp  7024  domen  7080  mapsnen  7143  xpsnen  7151  xpcomco  7157  xpassen  7161  sbthlem9  7184  frfi  7311  marypha2lem2  7399  epfrs  7623  tcsni  7638  cp  7771  bnd2  7773  dfac5lem1  7960  dfac5lem2  7961  dfac5lem5  7964  kmlem3  7988  dfackm  8002  cfval2  8096  cflim3  8098  cfss  8101  cfslb  8102  zfcndrep  8445  eltsk2g  8582  ltexpi  8735  recmulnq  8797  ltexprlem4  8872  addcnsr  8966  mulcnsr  8967  ltresr  8971  axrrecex  8994  elnnz  10248  elnn0z  10250  fnn0ind  10325  rexuz2  10484  rexrp  10587  elixx3g  10885  elfz2  11006  elfzuzb  11009  elfz2nn0  11038  fznn0  11069  fznn  11070  4fvwrd4  11076  elfzo2  11098  fzind2  11153  hashf1lem1  11659  hashf1lem2  11660  fz1isolem  11665  s4f1o  11820  fsum2dlem  12509  sinltx  12745  divalglem10  12877  divalgb  12879  isprm2  13042  infpn2  13236  prdsle  13639  prdsless  13640  prdsleval  13654  imasleval  13721  oppcsect  13954  elhoma  14142  ispos2  14360  tosso  14420  ismhm  14695  issubm  14703  submacs  14720  issubg  14899  issubg3  14915  gaorb  15039  efgcpbllema  15341  efgcpbllemb  15342  frgpuplem  15359  subgdmdprd  15547  dprd2d2  15557  dfrhm2  15776  drngprop  15801  drngid2  15806  opprdrng  15814  issubrg  15823  isabv  15862  islss  15966  islbs  16103  lsmspsn  16111  isassa  16330  aspval2  16360  ltbval  16487  opsrle  16491  opsrtoslem1  16499  isobs  16902  istps2OLD  16941  istps3OLD  16942  istps5OLD  16944  ntreq0  17096  restntr  17200  cnnei  17300  cnrest  17303  hausnei2  17371  cmpcov2  17407  cmpsub  17417  uncmp  17420  cmpfi  17425  llyi  17490  subislly  17497  iskgen3  17534  1stckgenlem  17538  ptpjpre1  17556  txcnpi  17593  txtube  17625  hausdiag  17630  txlm  17633  txkgen  17637  cfinfil  17878  csdfil  17879  supfil  17880  fin1aufil  17917  elflim2  17949  hauspwpwf1  17972  txflf  17991  isfcls  17994  alexsubALTlem3  18033  alexsubALT  18035  cnextcn  18051  istmd  18057  istgp  18060  tgphaus  18099  divstgplem  18103  istrg  18146  istdrg  18148  istlm  18167  blres  18414  isms2  18433  metrest  18507  metustidOLD  18542  metustid  18543  metuel2  18562  restmetu  18570  isngp  18596  isnlm  18664  elii1  18913  iscph  19086  cfilucfil3OLD  19224  cfilucfil3  19225  isbn  19244  limcrcl  19714  ig1pval3  20050  plydivex  20167  ellogdm  20483  cubic  20642  dmarea  20749  vmasum  20953  lgsquadlem1  21091  lgsquadlem2  21092  nb3graprlem2  21414  nb3grapr  21415  nb3grapr2  21416  nb3gra2nb  21417  cusgra2v  21424  trls  21489  3v3e3cycl2  21604  vdgrun  21625  vdgrfiun  21626  avril1  21710  islno  22207  h2hlm  22436  hcau  22639  hhsssh2  22723  dfch2  22862  elcnop  23313  ellnop  23314  elhmop  23329  elcnfn  23338  ellnfn  23339  dmadjss  23343  adjeu  23345  adjval  23346  hhcno  23360  hhcnf  23361  eleigvec  23413  isst  23669  ishst  23670  cvnbtwn3  23744  cvnbtwn4  23745  chirredi  23850  sumdmdii  23871  or3di  23904  rexunirn  23931  rmo3f  23935  rmo4fOLD  23936  ofpreima  24034  1stpreima  24048  2ndpreima  24049  sigaex  24445  sigaval  24446  isrnsigaOLD  24448  probun  24630  ballotlemelo  24698  ballotlem2  24699  ballotlemfc0  24703  ballotlemfcc  24704  erdszelem1  24830  iscvm  24899  dfso3  25130  coepr  25323  dfpo2  25326  dfdm5  25346  dfrn5  25347  preduz  25414  wfi  25421  frind  25457  soseq  25468  wfrlem11  25480  tfrALTlem  25490  frrlem5c  25501  elno3  25523  nofulllem5  25574  brtxp  25634  brpprod  25639  dfon3  25646  dffun10  25667  elfuns  25668  brimg  25690  brapply  25691  brcup  25692  brcap  25693  brsuccf  25694  funpartlem  25695  funpartfun  25696  brrestrict  25702  dfrdg4  25703  tfrqfree  25704  colinearalg  25753  axeuclid  25806  axcontlem2  25808  axcontlem5  25811  lineunray  25985  ellines  25990  rabiun2  26139  ismblfin  26146  ovoliunnfl  26147  voliunnfl  26149  volsupnfl  26150  itg2addnclem2  26156  itg2addnclem3  26157  itg2addnc  26158  finminlem  26211  fneval  26257  neibastop3  26281  isbnd2  26382  bndss  26385  heibor1lem  26408  heibor1  26409  isrngohom  26471  isidl  26514  prtlem70  26588  prtlem100  26594  prter2  26620  elmzpcl  26673  mzpindd  26693  fphpd  26767  pw2f1ocnv  26998  islmodfg  27035  islssfg2  27037  islinds  27147  isdomn3  27391  pm13.192  27478  rexdifpr  27947  nn0fz0  27979  usgra2pth0  28042  usg2spthonot0  28086  2pthfrgrarn  28113  opelopab4  28349  a9e2nd  28356  en3lplem2VD  28665  a9e2ndVD  28729  a9e2ndALT  28752  bnj248  28770  bnj250  28771  bnj268  28779  bnj312  28782  bnj945  28850  bnj110  28935  bnj849  29002  bnj882  29003  bnj893  29005  bnj916  29010  bnj983  29028  bnj1040  29047  bnj1175  29079  sb3anNEW7  29341  eeeanvOLD7  29388  lsateln0  29478  islshpat  29500  lcvnbtwn3  29511  islfl  29543  ishlat1  29835  ishlat2  29836  cvrat4  29925  islvol5  30061  psubspset  30226  snatpsubN  30232  dalawlem13  30365  psubclsetN  30418  isltrn2N  30602  cdlemftr3  31047  dibelval3  31630  dicval2  31662  dicopelval2  31664  dicelval2N  31665  dihglb2  31825  islpolN  31966  lcfls1c  32019  mapdvalc  32112  mapdval4N  32115  mapdordlem1a  32117
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