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

Theorem anbi1i 695
Description: Introduce a right conjunct to both sides of a logical equivalence. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)
Hypothesis
Ref Expression
anbi.1
Assertion
Ref Expression
anbi1i

Proof of Theorem anbi1i
StepHypRef Expression
1 anbi.1 . . 3
21a1i 11 . 2
32pm5.32ri 638 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369
This theorem is referenced by:  anbi2ci  696  anbi12i  697  pm5.53  796  an12  797  anandi  828  pm5.75  937  3ancoma  980  3ioran  991  3an4anass  1219  an6  1308  an3andi  1341  an33rean  1342  dfifp4  1384  dfifp5  1385  19.26-3an  1682  19.28v  1767  19.28  1924  eeeanv  1989  sb3an  2141  sbel2x  2203  2eu4  2380  2eu6OLD  2384  r19.26-3  2986  r19.41v  3009  r19.41  3010  rexcomf  3017  3reeanv  3026  cbvreu  3082  ceqsex3v  3149  rexab  3262  rexrab  3263  rmo4  3292  reuind  3303  sbc3an  3390  rmo3  3429  ssrab  3577  rexun  3683  elin3  3689  inass  3707  dfun2  3732  indifdir  3753  difin2  3759  inrab2  3770  rabun2  3776  reuun2  3780  undif4  3883  difin0ss  3894  rexsns  4062  rexsnsOLD  4063  rexdifsn  4159  2ralunsn  4238  iuncom4  4338  iunxiun  4413  disjxun  4450  zfrep4  4571  inuni  4614  reusv2lem4  4656  reusv2  4658  otth2  4733  copsexg  4737  copsexgOLD  4738  copsex4g  4741  opeqsn  4748  opelopabsbALT  4761  dfid3  4801  wefrc  4878  rabxp  5041  opeliunxp  5056  xpundir  5058  xpiundi  5059  xpiundir  5060  brinxp2  5066  copsex2gb  5118  brres  5285  brresg  5287  dmres  5299  restidsing  5335  dminss  5425  imainss  5426  difxp  5436  ssrnres  5450  cnvresima  5501  coundi  5513  resco  5516  imaco  5517  coiun  5522  coi1  5528  coass  5531  cnvpo  5550  xpco  5552  dffun2  5603  fncnv  5657  imadif  5668  mptun  5717  fcnvres  5767  dff1o2  5826  dff1o3  5827  brprcneu  5864  fvun2  5945  eqfnfv3  5983  respreima  6016  f1ompt  6053  fsn  6069  fmptsng  6092  fmptsnd  6093  abrexco  6156  imaiun  6157  f1mpt  6169  dff1o6  6181  oprabid  6323  dfoprab2  6343  oprab4  6368  mpt2mptx  6393  resiexg  6736  elxp4  6744  elxp5  6745  ffoss  6761  f11o  6762  opabex3d  6778  opabex3  6779  abexssex  6782  elxp7  6833  dfopab2  6854  dfoprab3s  6855  1stconst  6888  2ndconst  6889  frxp  6910  xporderlem  6911  suppssov1  6951  suppssfv  6955  brtpos2  6980  tpostpos  6994  tposmpt2  7011  oarec  7230  oeeu  7271  mapsncnv  7485  dfixp  7491  domen  7549  mapsnen  7613  xpsnen  7621  xpcomco  7627  xpassen  7631  sbthlem9  7655  frfi  7785  marypha2lem2  7916  epfrs  8183  tcsni  8195  cp  8330  bnd2  8332  dfac5lem1  8525  dfac5lem2  8526  dfac5lem5  8529  kmlem3  8553  dfackm  8567  cfval2  8661  cflim3  8663  cfss  8666  cfslb  8667  zfcndrep  9013  eltsk2g  9150  ltexpi  9301  recmulnq  9363  ltexprlem4  9438  addsrpr  9473  mulsrpr  9474  addcnsr  9533  mulcnsr  9534  ltresr  9538  axrrecex  9561  elnnz  10899  elnn0z  10902  fnn0ind  10988  rexuz2  11161  rexrp  11268  elixx3g  11571  elfz2  11708  elfzuzb  11711  fznn  11776  elfz2nn0  11798  fznn0  11799  4fvwrd4  11822  elfzo2  11832  fzind2  11924  hashf1lem1  12504  hashf1lem2  12505  fz1isolem  12510  s4f1o  12866  wwlktovfo  12896  fsum2dlem  13585  modfsummod  13608  sinltx  13924  divalglem10  14060  divalgb  14062  isprm2  14225  infpn2  14431  prdsle  14859  prdsless  14860  prdsleval  14874  imasleval  14938  oppcsect  15168  elhoma  15359  ispos2  15577  lubeldm  15611  glbeldm  15624  tosso  15666  ismhm  15968  issubm  15978  submacs  15996  issubg  16201  issubg3  16219  gaorb  16345  pmtrrn2  16485  efgcpbllema  16772  efgcpbllemb  16773  frgpuplem  16790  subgdmdprd  17081  dprd2d2  17093  dfrhm2  17366  drngprop  17407  drngid2  17412  opprdrng  17420  issubrg  17429  isabv  17468  islss  17581  islbs  17722  lsmspsn  17730  isassa  17964  aspval2  17996  ltbval  18136  opsrle  18140  opsrtoslem1  18148  isobs  18751  islinds  18844  fvmptnn04if  19350  istps2OLD  19422  istps3OLD  19423  istps5OLD  19425  ntreq0  19578  restntr  19683  cnnei  19783  hausnei2  19854  cmpcov2  19890  cmpsub  19900  uncmp  19903  cmpfi  19908  llyi  19975  subislly  19982  dissnlocfin  20030  iskgen3  20050  1stckgenlem  20054  ptpjpre1  20072  txcnpi  20109  txtube  20141  hausdiag  20146  txlm  20149  txkgen  20153  cfinfil  20394  csdfil  20395  supfil  20396  fin1aufil  20433  elflim2  20465  hauspwpwf1  20488  txflf  20507  isfcls  20510  alexsubALTlem3  20549  alexsubALT  20551  cnextcn  20567  istmd  20573  istgp  20576  tgphaus  20615  qustgplem  20619  istrg  20666  istdrg  20668  istlm  20687  blres  20934  isms2  20953  metrest  21027  metustidOLD  21062  metustid  21063  metuel2  21082  restmetu  21090  isngp  21116  isnlm  21184  elii1  21435  iscph  21617  cfilucfil3OLD  21757  cfilucfil3  21758  isbn  21777  limcrcl  22278  ig1pval3  22575  plydivex  22693  ellogdm  23020  cubic  23180  dmarea  23287  vmasum  23491  lgsquadlem1  23629  lgsquadlem2  23630  legov  23972  ltgov  23983  colinearalg  24213  axeuclid  24266  axcontlem2  24268  axcontlem5  24271  nb3graprlem2  24452  nb3grapr  24453  nb3grapr2  24454  nb3gra2nb  24455  cusgra2v  24462  trls  24538  3v3e3cycl2  24664  wwlknprop  24686  wlknwwlknsur  24712  wlkiswwlksur  24719  wwlkextsur  24731  wwlknfi  24738  wlknwwlknvbij  24740  clwwlkvbij  24801  erclwwlkref  24813  erclwwlknref  24825  usg2spthonot0  24889  vdgrun  24901  vdgrfiun  24902  2pthfrgrarn  25009  frgrareg  25117  frgraregord013  25118  avril1  25171  islno  25668  h2hlm  25897  hcau  26101  hhsssh2  26186  dfch2  26325  elcnop  26776  ellnop  26777  elhmop  26792  elcnfn  26801  ellnfn  26802  dmadjss  26806  adjeu  26808  adjval  26809  hhcno  26823  hhcnf  26824  eleigvec  26876  isst  27132  ishst  27133  cvnbtwn3  27207  cvnbtwn4  27208  chirredi  27313  sumdmdii  27334  or3di  27367  spc2ed  27372  rexunirn  27390  rmo3f  27394  rmo4fOLD  27395  rabrab  27399  disjunsn  27453  opeldifid  27456  ofpreima  27507  mpt2mptxf  27518  1stpreima  27524  2ndpreima  27525  f1od2  27547  resf1o  27553  maprnin  27554  nndiffz1  27596  omndmul2  27702  isorng  27789  pcmplfin  27863  ordtconlem1  27906  isrrext  27981  sigaex  28109  sigaval  28110  isrnsigaOLD  28112  eulerpartleme  28302  eulerpartlemt0  28308  eulerpartlemr  28313  eulerpartlemn  28320  probun  28358  ballotlemelo  28426  ballotlem2  28427  ballotlemfc0  28431  ballotlemfcc  28432  erdszelem1  28635  iscvm  28704  elmpst  28896  mpstrcl  28901  dfso3  29097  coepr  29181  dfpo2  29184  dfdm5  29206  dfrn5  29207  elima4  29209  preduz  29280  wfi  29287  frind  29323  soseq  29334  wfrlem11  29353  wzel  29380  frrlem5c  29393  elno3  29415  nofulllem5  29466  brtxp  29530  brpprod  29535  dfon3  29542  elfix  29553  dffix2  29555  sscoid  29563  elfuns  29565  brimg  29587  brapply  29588  brsuccf  29591  funpartlem  29592  funpartfun  29593  brrestrict  29599  dfrdg4  29600  tfrqfree  29601  lineunray  29797  ellines  29802  rabiun  30036  iundif1  30037  ismblfin  30055  ovoliunnfl  30056  voliunnfl  30058  volsupnfl  30059  itg2addnclem2  30067  itg2addnclem3  30068  itg2addnc  30069  ftc1anc  30098  finminlem  30136  fneval  30170  neibastop3  30180  isbnd2  30279  bndss  30282  heibor1lem  30305  heibor1  30306  isrngohom  30368  isidl  30411  sbccom2lem  30529  prtlem70  30592  prtlem100  30596  prter2  30622  elmzpcl  30658  mzpindd  30678  fphpd  30750  pw2f1ocnv  30979  islmodfg  31015  islssfg2  31017  isdomn3  31164  pm13.192  31317  limcrecl  31635  dvnprodlem2  31744  fourierdlem103  31992  fourierdlem104  31993  rexdifpr  32300  usgra2pth0  32355  xpsnopab  32453  ismgmhm  32471  issubmgm  32477  submgmacs  32492  sgrp2sgrp  32552  tpres  32554  dfiso2  32568  opeliun2xp  32922  mpt2mptx2  32924  lindslinindsimp1  33058  lindslinindsimp2  33064  alsconv  33205  aacllem  33216  opelopab4  33324  ax6e2nd  33331  en3lplem2VD  33644  ax6e2ndVD  33708  ax6e2ndALT  33730  bnj248  33752  bnj250  33753  bnj268  33761  bnj312  33764  bnj945  33832  bnj110  33916  bnj849  33983  bnj882  33984  bnj893  33986  bnj916  33991  bnj983  34009  bnj1040  34028  bnj1175  34060  bj-inrab  34495  bj-elid3  34601  lsateln0  34720  islshpat  34742  lcvnbtwn3  34753  islfl  34785  ishlat1  35077  ishlat2  35078  cvrat4  35167  islvol5  35303  psubspset  35468  snatpsubN  35474  dalawlem13  35607  psubclsetN  35660  isltrn2N  35844  cdlemftr3  36291  dibelval3  36874  dicval2  36906  dicopelval2  36908  dicelval2N  36909  dihglb2  37069  islpolN  37210  lcfls1c  37263  mapdvalc  37356  mapdval4N  37359  mapdordlem1a  37361  rp-fakeoranass  37738  rp-isfinite6  37744
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 185  df-an 371
  Copyright terms: Public domain W3C validator