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

Theorem anbi2i 694
Description: Introduce a left conjunct to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)
Hypothesis
Ref Expression
anbi.1
Assertion
Ref Expression
anbi2i

Proof of Theorem anbi2i
StepHypRef Expression
1 anbi.1 . . 3
21a1i 11 . 2
32pm5.32i 637 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369
This theorem is referenced by:  anbi12i  697  an4  824  an42  825  anandir  829  dfbi3  893  dn1  966  an3andi  1341  an33rean  1342  nannanOLD  1349  anxordi  1378  dfifp3  1383  cadcoma  1462  nic-mpALT  1505  nic-axALT  1507  19.35OLD  1688  19.27v  1766  19.41v  1771  3exdistr  1780  4exdistr  1781  equvin  1804  19.27  1923  19.41  1971  sbn  2132  2sb5  2187  eu5  2310  eu3v  2312  eu2  2326  eu3OLD  2329  eu5OLD  2330  mo4f  2336  eu4  2338  2mos  2375  2eu4  2380  2eu4OLD  2381  2eu6OLD  2384  clelabOLD  2602  nonconneOLD  2666  rexbii  2959  r2exfOLD  2979  ceqsex3v  3149  ceqsex4v  3150  ceqsex8v  3152  reu2  3287  reu6  3288  reu4  3293  reu7  3294  2reu5lem3  3307  2reu5  3308  rmo3  3429  dfpss2  3588  difdif  3629  raldifb  3643  inass  3707  dfss4  3731  dfin2  3733  indi  3743  indifdir  3753  difin0ss  3894  inssdif0  3895  ssunpr  4192  unipr  4262  uniun  4268  uniin  4269  csbuni  4277  iunin2  4394  iundif2  4397  iindif2  4399  iinin2  4400  axrep1  4564  axrep4  4567  notzfaus  4627  reusv2lem4  4656  eqvinop  4736  opcom  4746  opeqsn  4748  ordtri3or  4915  fconstmpt  5048  opeliunxp  5056  xpundi  5057  elvvv  5064  xpiindi  5143  elcnv2  5185  cnvuni  5194  dmuni  5217  opelres  5284  elima3  5349  imai  5354  imainss  5426  difxp  5436  xpdifid  5440  ssrnres  5450  cnvresima  5501  mptpreima  5505  coundir  5514  rnco  5518  coass  5531  relrelss  5536  dffun2  5603  dffun3  5604  dffun4  5605  dffun5  5606  dffun6f  5607  dffun7  5619  dffun8  5620  dffun9  5621  svrelfun  5656  fncnv  5657  imadif  5668  dfmpt3  5708  fint  5769  fin  5770  dff12  5785  fores  5809  dff1o4  5829  eqfnfv3  5983  fndmin  5994  fniniseg  6008  rexsuppOLD  6012  unpreima  6013  ffnfvf  6058  fsn2  6071  fconstfv  6133  dff13f  6167  dff14a  6177  dff14b  6178  isocnv2  6227  ffnov  6406  eqfnov  6408  foov  6449  uniuni  6609  tfindsg  6695  findsg  6727  funcnvuni  6753  opabex3d  6778  opabex3  6779  frxp  6910  soxp  6913  suppvalbr  6922  mpt2xopovel  6967  brtpos  6983  tpostpos  6994  dfsmo2  7037  rdglem1  7100  tz7.49  7129  brwitnlem  7176  oeeu  7271  erinxp  7404  mapsncnv  7485  cbvixp  7506  ixpin  7514  ixpiin  7515  mptelixpg  7526  elixpsn  7528  ixpsnf1o  7529  mapsnen  7613  xpassen  7631  omxpenlem  7638  sbthcl  7659  dfsup2OLD  7923  wemapsolem  7996  dford2  8058  inf2  8061  zfinf  8077  trcl  8180  iscard2  8378  leweon  8410  aceq1  8519  dfac3  8523  dfac4  8524  dfac5lem2  8526  dfac5lem3  8527  dfac5  8530  kmlem3  8553  kmlem4  8554  kmlem14  8564  kmlem15  8565  dfackm  8567  infmap2  8619  cf0  8652  fin23lem25  8725  zorn2lem7  8903  brdom6disj  8931  zfcndrep  9013  zfcndinf  9017  fpwwe  9045  axgroth4  9231  grothprim  9233  grothtsk  9234  nqpr  9413  addsrmo  9471  mulsrmo  9472  opelreal  9528  elnnz  10899  elznn0nn  10903  peano2uz2  10975  nnwos  11178  dflt2  11383  xmullem  11485  elfzuzb  11711  4fvwrd4  11822  elfznelfzo  11915  fzind2  11924  fsuppmapnn0fiubex  12098  hashinfxadd  12453  hashfun  12495  brfi1uzind  12532  shftdm  12904  rexfiuz  13180  cbvsum  13517  mertenslem2  13694  mertens  13695  cbvprod  13722  prodmo  13743  iprodmul  13796  divalglem10  14060  ndvdssub  14065  bitsmod  14086  algcvgblem  14206  isprm2  14225  isprm4  14227  hashdvds  14305  infpn2  14431  hashbc0  14523  xpscf  14963  funcpropd  15269  isffth2  15285  eldmcoa  15392  setcinv  15417  xpccatid  15457  yonedainv  15550  ispos  15576  ispos2  15577  joinfval2  15632  meetfval2  15646  istsr2  15848  isnsg2  16231  isnsg4  16244  isgim  16310  oppgid  16391  oppgcntz  16399  symgfix2  16441  efgval2  16742  iscyg2  16885  dmdprdd  17030  subgdmdprd  17081  issrg  17159  oppr1  17283  opprunit  17310  opprirred  17351  isrhm  17370  subsubrg2  17456  islmim  17708  lbsextg  17808  lidlnz  17876  isdomn2  17948  opsrtoslem1  18148  resubdrg  18644  unocv  18711  pjfval2  18740  islinds2  18848  mdetunilem8  19121  fvmptnn04if  19350  istop2g  19405  istps4OLD  19424  isbasis2g  19449  tgval2  19457  isclo2  19589  isnrm2  19859  is1stc2  19943  llyi  19975  isfbas2  20336  elfg  20372  ufinffr  20430  isfcls  20510  alexsubALTlem2  20548  alexsubALTlem3  20549  cnextcn  20567  ustfilxp  20715  iscusp2  20805  elcncf1di  21399  tchcph  21680  iscau3  21717  caucfil  21722  ellogdm  23020  dvdsflsumcom  23464  logfac2  23492  dchrelbas3  23513  dchrvmasumlema  23685  legtrid  23978  axcontlem5  24271  axcontlem6  24272  axcontlem7  24273  nb3grapr2  24454  uvtx01vtx  24492  3v3e3cycl2  24664  wwlkn0s  24705  wwlkextwrd  24728  usg2spthonot0  24889  rusgranumwlkl1  24947  frgra3v  25002  4cycl2vnunb  25017  usg2spot2nb  25065  numclwwlkovf2  25084  numclwwlk3lem  25108  isgrpo2  25199  hhcms  26120  isch3  26159  ocsh  26201  pjhtheu  26312  pjpreeq  26316  h1deoi  26467  h1dei  26468  eleigvec  26876  cvbr2  27202  cvnbtwn2  27206  cvnbtwn4  27208  mdsl2i  27241  cvmdi  27243  mdsymlem6  27327  cdj3lem3b  27359  mo5f  27383  nmo  27384  rexunirn  27390  rmo3f  27394  rmo4fOLD  27395  rmo4f  27396  disjunsn  27453  unipreima  27484  dfcnv2  27517  1stpreima  27524  isrnsigaOLD  28112  isrnsiga  28113  eulerpartlemr  28313  eulerpartlemgvv  28315  ballotlemodife  28436  plymulx  28505  signstfvneq0  28529  erdszelem9  28643  cvmlift2lem9  28756  cvmlift2lem13  28760  elmthm  28936  axinfprim  29078  axacprim  29079  coep  29180  dfso2  29183  dford5reg  29214  dfon2lem5  29219  dfon2  29224  preduz  29280  wfi  29287  trpredmintr  29314  frind  29323  frr3g  29386  brtxp2  29531  brpprod3a  29536  dfom5b  29562  brcart  29582  brimg  29587  brsuccf  29591  funpartlem  29592  cgrxfr  29705  segletr  29764  df3nandALT1  29862  andnand1  29864  nandsym1  29887  finixpnum  30038  ptrest  30048  cnambfre  30063  itg2addnc  30069  ftc1anc  30098  trer  30134  fneval  30170  neifg  30189  opropabco  30214  f1opr  30215  isdrngo1  30359  keridl  30429  ispridlc  30467  selconj  30500  mergeconj  30502  an43OLD  30590  prtlem70  30592  prtlem100  30596  prtlem15  30616  mzpcompact2lem  30684  fz1eqin  30702  rexrabdioph  30727  expdiophlem1  30963  dford4  30971  fnwe2lem2  30997  fgraphopab  31170  2sbc5g  31323  pm14.12  31328  cncfshift  31676  dvnmul  31740  dvnprodlem2  31744  stoweidlem26  31808  stoweidlem35  31817  fourierdlem54  31943  fourierdlem83  31972  fourierdlem100  31989  fourierdlem104  31993  fourierdlem109  31998  fourierdlem112  32001  reuan  32185  2reu4a  32194  dfdfat2  32216  ffnaov  32284  rexdifpr  32300  tpres  32554  isrnghm  32698  2zrngmmgm  32752  rngcinv  32789  rngcinvOLD  32801  ringcinv  32840  ringcinvOLD  32864  opeliun2xp  32922  pgrpgt2nabl  32959  islindeps  33054  lindslinindsimp1  33058  lindslinindsimp2  33064  ldepslinc  33110  2sb5nd  33333  uun2221  33610  uun2221p1  33611  uun2221p2  33612  2sb5ndVD  33710  2sb5ndALT  33732  bnj251  33754  bnj252  33755  bnj257  33759  bnj290  33762  bnj1304  33878  bnj153  33938  bnj543  33951  bnj571  33964  bnj580  33971  bnj607  33974  bnj882  33984  bnj964  34001  bnj996  34013  bnj1033  34025  bnj1176  34061  bnj1186  34063  bnj1189  34065  bnj1204  34068  bnj1253  34073  bnj1452  34108  bnj1463  34111  bj-axrep1  34374  bj-axrep4  34377  bj-eu3f  34413  bj-csbsnlem  34470  bj-snsetex  34521  bj-elsngl  34526  bj-snglc  34527  islshpat  34742  lcvbr2  34747  lcvbr3  34748  lcvnbtwn2  34752  ellkr  34814  cvrval2  34999  cvrnbtwn2  35000  cvrnbtwn3  35001  cvrnbtwn4  35004  ishlat2  35078  lplnexatN  35287  islvol5  35303  dath  35460  pmapglb  35494  polval2N  35630  pclfinclN  35674  lhpexle3  35736  4atex2  35801  4atex2-0bOLDN  35803  isltrn2N  35844  cdleme0nex  36015  cdleme22b  36067  cdlemg17pq  36398  cdlemg19  36410  cdlemg21  36412  cdlemg33d  36435  dibopelvalN  36870  dibopelval2  36872  dib1dim  36892  dicelval2N  36909  diclspsn  36921  lcdlss  37346  mapd1o  37375  bj-ifidg  37707  rp-fakenanass  37739  rp-fakeinunass  37740  rp-isfinite6  37744  cotr2g  37786
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