MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  anbi1i Structured version   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  1605  19.28  1842  eeeanv  1938  eeeanvOLD  1939  sb3an  2144  pm11.07OLD  2191  2eu6  2365  r19.26-3  2832  r19.41  2852  rexcomf  2859  3reeanv  2868  cbvreu  2922  ceqsex3v  2986  rexab  3089  rexrab  3090  rmo4  3119  reuind  3129  rmo3  3240  ssrab  3413  rexun  3519  elin3  3524  inass  3543  dfun2  3568  indifdir  3589  difin2  3595  inrab2  3606  rabun2  3612  reuun2  3616  undif4  3676  difin0ss  3686  rexsns  3837  rexdifsn  3923  2ralunsn  3996  iuncom4  4092  iunxiun  4165  disjxun  4202  zfrep4  4320  inuni  4354  otth2  4431  copsexg  4434  copsex4g  4437  opeqsn  4444  opelopabsbOLD  4455  dfid3  4491  wefrc  4568  reusv2lem4  4719  reusv2  4721  rabxp  4906  opeliunxp  4921  xpundir  4923  xpiundi  4924  xpiundir  4925  brinxp2  4931  brres  5144  brresg  5146  dmres  5159  resiexg  5180  dminss  5278  imainss  5279  ssrnres  5301  elxp4  5349  elxp5  5350  cnvresima  5351  coundi  5363  resco  5366  imaco  5367  coiun  5371  coi1  5377  coass  5380  cnvpo  5402  xpco  5406  dffun2  5456  fncnv  5507  imadif  5520  mptun  5567  fcnvres  5612  dff1o2  5671  dff1o3  5672  ffoss  5699  f11o  5700  brprcneu  5713  fvun2  5787  eqfnfv3  5821  respreima  5851  f1ompt  5883  fsn  5898  abrexco  5978  opabex3d  5981  opabex3  5982  imaiun  5984  abexssex  5994  f1mpt  5999  dff1o6  6005  oprabid  6097  dfoprab2  6113  oprab4  6135  mpt2mptx  6156  elxp7  6371  difxp  6372  dfopab2  6393  dfoprab3s  6394  copsex2gb  6399  1stconst  6427  2ndconst  6428  frxp  6448  xporderlem  6449  brtpos2  6477  tpostpos  6491  tposmpt2  6508  oarec  6797  oeeui  6837  oeeu  6838  ovec  7006  map0e  7043  mapsncnv  7052  dfixp  7057  domen  7113  mapsnen  7176  xpsnen  7184  xpcomco  7190  xpassen  7194  sbthlem9  7217  frfi  7344  marypha2lem2  7433  epfrs  7657  tcsni  7672  cp  7805  bnd2  7807  dfac5lem1  7994  dfac5lem2  7995  dfac5lem5  7998  kmlem3  8022  dfackm  8036  cfval2  8130  cflim3  8132  cfss  8135  cfslb  8136  zfcndrep  8479  eltsk2g  8616  ltexpi  8769  recmulnq  8831  ltexprlem4  8906  addcnsr  9000  mulcnsr  9001  ltresr  9005  axrrecex  9028  elnnz  10282  elnn0z  10284  fnn0ind  10359  rexuz2  10518  rexrp  10621  elixx3g  10919  elfz2  11040  elfzuzb  11043  elfz2nn0  11072  fznn0  11103  fznn  11105  4fvwrd4  11111  elfzo2  11133  fzind2  11188  hashf1lem1  11694  hashf1lem2  11695  fz1isolem  11700  s4f1o  11855  fsum2dlem  12544  sinltx  12780  divalglem10  12912  divalgb  12914  isprm2  13077  infpn2  13271  prdsle  13674  prdsless  13675  prdsleval  13689  imasleval  13756  oppcsect  13989  elhoma  14177  ispos2  14395  tosso  14455  ismhm  14730  issubm  14738  submacs  14755  issubg  14934  issubg3  14950  gaorb  15074  efgcpbllema  15376  efgcpbllemb  15377  frgpuplem  15394  subgdmdprd  15582  dprd2d2  15592  dfrhm2  15811  drngprop  15836  drngid2  15841  opprdrng  15849  issubrg  15858  isabv  15897  islss  16001  islbs  16138  lsmspsn  16146  isassa  16365  aspval2  16395  ltbval  16522  opsrle  16526  opsrtoslem1  16534  isobs  16937  istps2OLD  16976  istps3OLD  16977  istps5OLD  16979  ntreq0  17131  restntr  17236  cnnei  17336  cnrest  17339  hausnei2  17407  cmpcov2  17443  cmpsub  17453  uncmp  17456  cmpfi  17461  llyi  17527  subislly  17534  iskgen3  17571  1stckgenlem  17575  ptpjpre1  17593  txcnpi  17630  txtube  17662  hausdiag  17667  txlm  17670  txkgen  17674  cfinfil  17915  csdfil  17916  supfil  17917  fin1aufil  17954  elflim2  17986  hauspwpwf1  18009  txflf  18028  isfcls  18031  alexsubALTlem3  18070  alexsubALT  18072  cnextcn  18088  istmd  18094  istgp  18097  tgphaus  18136  divstgplem  18140  istrg  18183  istdrg  18185  istlm  18204  blres  18451  isms2  18470  metrest  18544  metustidOLD  18579  metustid  18580  metuel2  18599  restmetu  18607  isngp  18633  isnlm  18701  elii1  18950  iscph  19123  cfilucfil3OLD  19261  cfilucfil3  19262  isbn  19281  limcrcl  19751  ig1pval3  20087  plydivex  20204  ellogdm  20520  cubic  20679  dmarea  20786  vmasum  20990  lgsquadlem1  21128  lgsquadlem2  21129  nb3graprlem2  21451  nb3grapr  21452  nb3grapr2  21453  nb3gra2nb  21454  cusgra2v  21461  trls  21526  3v3e3cycl2  21641  vdgrun  21662  vdgrfiun  21663  avril1  21747  islno  22244  h2hlm  22473  hcau  22676  hhsssh2  22760  dfch2  22899  elcnop  23350  ellnop  23351  elhmop  23366  elcnfn  23375  ellnfn  23376  dmadjss  23380  adjeu  23382  adjval  23383  hhcno  23397  hhcnf  23398  eleigvec  23450  isst  23706  ishst  23707  cvnbtwn3  23781  cvnbtwn4  23782  chirredi  23887  sumdmdii  23908  or3di  23941  rexunirn  23968  rmo3f  23972  rmo4fOLD  23973  ofpreima  24071  1stpreima  24085  2ndpreima  24086  sigaex  24482  sigaval  24483  isrnsigaOLD  24485  probun  24667  ballotlemelo  24735  ballotlem2  24736  ballotlemfc0  24740  ballotlemfcc  24741  erdszelem1  24867  iscvm  24936  dfso3  25167  coepr  25365  dfpo2  25368  dfdm5  25388  dfrn5  25389  elima4  25392  preduz  25460  wfi  25467  frind  25503  soseq  25514  wfrlem11  25533  tfrALTlem  25542  frrlem5c  25553  elno3  25575  nofulllem5  25626  brtxp  25690  brpprod  25695  dfon3  25702  elfix  25713  dffix2  25715  sscoid  25723  elfuns  25725  brimg  25747  brapply  25748  brsuccf  25751  funpartlem  25752  funpartfun  25753  brrestrict  25759  dfrdg4  25760  tfrqfree  25761  colinearalg  25814  axeuclid  25867  axcontlem2  25869  axcontlem5  25872  lineunray  26046  ellines  26051  rabiun2  26203  ismblfin  26210  ovoliunnfl  26211  voliunnfl  26213  volsupnfl  26214  itg2addnclem2  26220  itg2addnclem3  26221  itg2addnc  26222  finminlem  26275  fneval  26321  neibastop3  26345  isbnd2  26446  bndss  26449  heibor1lem  26472  heibor1  26473  isrngohom  26535  isidl  26578  prtlem70  26652  prtlem100  26658  prter2  26684  elmzpcl  26737  mzpindd  26757  fphpd  26831  pw2f1ocnv  27062  islmodfg  27099  islssfg2  27101  islinds  27211  isdomn3  27455  pm13.192  27542  rexdifpr  28013  usgra2pth0  28229  usg2spthonot0  28273  2pthfrgrarn  28300  4an31  28482  opelopab4  28539  a9e2nd  28546  en3lplem2VD  28857  a9e2ndVD  28921  a9e2ndALT  28943  bnj248  28965  bnj250  28966  bnj268  28974  bnj312  28977  bnj945  29045  bnj110  29130  bnj849  29197  bnj882  29198  bnj893  29200  bnj916  29205  bnj983  29223  bnj1040  29242  bnj1175  29274  sb3anNEW7  29541  eeeanvOLD7  29605  lsateln0  29694  islshpat  29716  lcvnbtwn3  29727  islfl  29759  ishlat1  30051  ishlat2  30052  cvrat4  30141  islvol5  30277  psubspset  30442  snatpsubN  30448  dalawlem13  30581  psubclsetN  30634  isltrn2N  30818  cdlemftr3  31263  dibelval3  31846  dicval2  31878  dicopelval2  31880  dicelval2N  31881  dihglb2  32041  islpolN  32182  lcfls1c  32235  mapdvalc  32328  mapdval4N  32331  mapdordlem1a  32333
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