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

Theorem anbi2i 611
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 566 1 ((𝜒𝜑) ↔ (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 197  wa 384
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 198  df-an 385
This theorem is referenced by:  anbi12i  614  bianass  625  an4  638  an42  639  anandir  659  annotanannotOLD  1025  dfbi3  1063  dfbi3OLD  1064  dn1  1073  dfifp3  1081  an3andi  1599  an33rean  1600  anxordi  1633  cadcoma  1706  nic-mpALT  1752  nic-axALT  1754  3exdistr  2049  4exdistr  2050  19.27v  2087  19.41vOLD  2093  19.27  2263  19.41  2271  2sb5  2288  19.27OLD  2408  sbn  2550  eu5  2658  eu3v  2660  eu2  2672  mo4f  2679  eu4  2681  2mos  2716  2eu4  2720  rexbii  3229  ceqsex3v  3440  ceqsex4v  3441  ceqsex8v  3443  reu2  3592  reu6  3593  reu4  3598  reu7  3599  2reu5lem3  3613  2reu5  3614  rmo3  3723  dfpss2  3890  difdif  3935  raldifb  3949  inass  4020  dfss4  4060  dfin2  4062  indi  4075  indifdir  4085  undif3  4090  difin0ss  4147  inssdif0  4148  rexdifpr  4399  ssdifsn  4509  ssunpr  4553  unipr  4643  uniun  4651  uniin  4652  csbuni  4660  iunin2  4776  iundif2  4779  iindif2  4781  iinin2  4782  elpwpw  4805  axrep1  4965  axrep4  4969  notzfaus  5032  reusv2lem4  5070  eqvinop  5144  opcom  5154  opeqsnOLD  5158  snopeqopOLD  5161  fconstmpt  5363  opeliunxp  5370  xpundi  5371  elvvv  5378  opelinxp  5383  xpiindi  5459  elcnv2  5501  cnvuni  5510  dmuni  5535  opelresOLD  5607  elidinxp  5660  elridOLD  5663  elima3  5683  imai  5688  imainss  5759  difxp  5769  xpdifid  5773  ssrnres  5783  mptpreima  5842  coundir  5851  rnco  5855  coass  5868  relrelss  5873  wfi  5926  ordtri3or  5968  dffun2  6111  dffun3  6112  dffun4  6113  dffun5  6114  dffun6f  6115  dffun7  6128  dffun8  6129  dffun9  6130  svrelfun  6172  fncnv  6173  imadif  6184  dfmpt3  6225  fint  6299  fin  6300  dff12  6315  fores  6340  dff1o4  6361  eqfnfv3  6535  fndmin  6546  fniniseg  6560  unpreima  6563  ffnfvf  6611  fsn2  6626  tpres  6691  fconstfv  6701  dff13f  6737  dff14a  6751  dff14b  6752  isocnv2  6805  ffnov  6994  eqfnov  6996  foov  7038  uniuni  7201  tfindsg  7290  findsg  7323  funcnvuni  7349  opabex3d  7375  opabex3  7376  frxp  7521  soxp  7524  suppvalbr  7533  mpt2xopovel  7581  brtpos  7596  tpostpos  7607  dfsmo2  7680  dfrecs3  7705  rdglem1  7747  tz7.49  7776  brwitnlem  7824  oeeu  7920  erinxp  8056  mapsncnv  8141  cbvixp  8162  ixpin  8170  ixpiin  8171  mptelixpg  8182  elixpsn  8184  ixpsnf1o  8185  xpassen  8293  omxpenlem  8300  sbthcl  8321  wemapsolem  8694  dford2  8764  inf2  8767  zfinf  8783  trcl  8851  iscard2  9085  leweon  9117  aceq1  9223  dfac3  9227  dfac4  9228  dfac5lem2  9230  dfac5lem3  9231  dfac5  9234  kmlem3  9259  kmlem4  9260  kmlem14  9270  kmlem15  9271  dfackm  9273  infmap2  9325  cf0  9358  fin23lem25  9431  zorn2lem7  9609  brdom6disj  9639  zfcndrep  9721  zfcndinf  9725  fpwwe  9753  axgroth4  9939  grothprim  9941  grothtsk  9942  nqpr  10121  addsrmo  10179  mulsrmo  10180  opelreal  10236  elnnz  11653  elznn0nn  11657  peano2uz2  11731  nnwos  11974  dflt2  12197  xmullem  12312  elfzuzb  12559  4fvwrd4  12683  preduz  12685  elfznelfzo  12797  fzind2  12810  fsuppmapnn0fiubex  13015  hashinfxadd  13392  hashfun  13441  fi1uzind  13496  brfi1uzind  13497  opfi1uzind  13500  cotr2g  13940  shftdm  14034  rexfiuz  14310  cbvsum  14648  mertenslem2  14838  mertens  14839  cbvprod  14866  prodmo  14887  iprodmul  14954  divalglem10  15345  ndvdssub  15352  bitsmod  15377  algcvgblem  15509  isprm2  15613  isprm4  15615  hashdvds  15697  infpn2  15834  hashbc0  15926  xpscf  16431  funcpropd  16764  isffth2  16780  eldmcoa  16919  setcinv  16944  xpccatid  17033  yonedainv  17126  ispos  17152  ispos2  17153  joinfval2  17207  meetfval2  17221  istsr2  17423  isnsg2  17826  isnsg4  17839  isgim  17906  oppgid  17987  oppgcntz  17995  symgfix2  18037  efgval2  18338  iscyg2  18485  dmdprdd  18600  subgdmdprd  18635  issrg  18709  oppr1  18836  opprunit  18863  opprirred  18904  isrhm  18925  subsubrg2  19011  islmim  19269  lbsextg  19371  lidlnz  19437  isdomn2  19508  opsrtoslem1  19692  resubdrg  20163  unocv  20234  pjfval2  20263  islinds2  20362  mdetunilem8  20636  fvmptnn04if  20867  istop2g  20914  isbasis2g  20966  tgval2  20974  isclo2  21106  isnrm2  21376  is1stc2  21459  llyi  21491  isfbas2  21852  elfg  21888  ufinffr  21946  isfcls  22026  alexsubALTlem2  22065  alexsubALTlem3  22066  cnextcn  22084  ustfilxp  22229  iscusp2  22319  elcncf1di  22911  isclmp  23109  iscvsp  23140  tchcph  23248  iscau3  23288  caucfil  23293  ellogdm  24599  dvdsflsumcom  25128  logfac2  25156  dchrelbas3  25177  dchrvmasumlema  25403  legtrid  25700  outpasch  25861  axcontlem5  26062  axcontlem6  26063  axcontlem7  26064  nb3grpr2  26501  iscplgr  26538  pthdlem1  26890  wwlksnextinj  27036  usgr2wspthon  27107  rusgrnumwwlkl1  27110  isclwwlk  27127  clwwlkccatlem  27132  clwwlknon2x  27271  iseupthf1o  27375  frcond3  27444  frgr3v  27450  4cycl2vnunb  27465  frgrncvvdeqlem2  27475  fusgr2wsp2nb  27509  numclwlk1lem1  27549  numclwwlk3lemOLD  27569  hhcms  28388  isch3  28426  ocsh  28470  pjhtheu  28581  pjpreeq  28585  h1deoi  28736  h1dei  28737  eleigvec  29144  cvbr2  29470  cvnbtwn2  29474  cvnbtwn4  29476  mdsl2i  29509  cvmdi  29511  mdsymlem6  29595  cdj3lem3b  29627  mo5f  29652  nmo  29653  rexunirn  29657  rmo3f  29661  rmo4fOLD  29662  rmo4f  29663  difrab2  29664  disjunsn  29732  unipreima  29773  dfcnv2  29803  1stpreima  29811  isrnsigaOLD  30500  isrnsiga  30501  rossros  30568  omsmeas  30710  eulerpartlemr  30761  eulerpartlemgvv  30763  ballotlemodife  30884  plymulx  30950  signstfvneq0  30974  bnj251  31093  bnj252  31094  bnj257  31098  bnj290  31101  bnj1304  31213  bnj153  31273  bnj543  31286  bnj571  31299  bnj580  31306  bnj607  31309  bnj882  31319  bnj964  31336  bnj996  31348  bnj1033  31360  bnj1176  31396  bnj1186  31398  bnj1189  31400  bnj1204  31403  bnj1253  31408  bnj1452  31443  bnj1463  31446  erdszelem9  31504  cvmlift2lem9  31616  cvmlift2lem13  31620  elmthm  31796  axinfprim  31905  axacprim  31906  coep  31963  dfso2  31966  fv1stcnv  32000  fv2ndcnv  32001  dford5reg  32007  dfon2lem5  32012  dfon2  32017  trpredmintr  32051  frpoind  32061  frind  32064  frr3g  32100  nosupno  32170  dmscut  32239  brtxp2  32309  brpprod3a  32314  dfom5b  32340  brcart  32360  brimg  32365  funpartlem  32370  dfrecs2  32378  cgrxfr  32483  segletr  32542  trer  32631  fneval  32668  neifg  32687  df3nandALT1  32715  andnand1  32717  nandsym1  32738  bj-dfssb2  32955  bj-axrep1  33102  bj-axrep4  33105  bj-eu3f  33142  bj-cleljustab  33159  bj-csbsnlem  33206  bj-snsetex  33261  bj-elsngl  33266  bj-snglc  33267  bj-restuni  33361  bj-ismooredr2  33376  bj-dfmpt2a  33382  mptsnunlem  33502  icorempt2  33515  isbasisrelowllem2  33520  relowlpssretop  33528  rdgeqoa  33534  dffinxpf  33538  curf  33700  finixpnum  33707  ptrest  33721  poimirlem1  33723  poimirlem14  33736  poimirlem16  33738  poimirlem19  33741  poimirlem25  33747  poimirlem26  33748  poimirlem27  33749  poimir  33755  cnambfre  33770  itg2addnc  33776  ftc1anc  33805  opropabco  33830  f1opr  33831  isdrngo1  34066  keridl  34142  ispridlc  34180  selconj  34213  anbi1ci  34317  brresALTV  34350  eldmqsres  34368  cnvepres  34383  ecinn0  34431  alrmomorn  34436  moantr  34440  dfxrn2  34451  inxpxrn  34466  rnxrnres  34470  prtlem70  34635  prtlem100  34638  prtlem15  34654  islshpat  34797  lcvbr2  34802  lcvbr3  34803  lcvnbtwn2  34807  ellkr  34869  cvrval2  35054  cvrnbtwn2  35055  cvrnbtwn3  35056  cvrnbtwn4  35059  ishlat2  35133  lplnexatN  35343  islvol5  35359  dath  35516  pmapglb  35550  polval2N  35686  pclfinclN  35730  lhpexle3  35792  4atex2  35857  4atex2-0bOLDN  35859  isltrn2N  35900  cdleme0nex  36071  cdleme22b  36122  cdlemg17pq  36453  cdlemg19  36465  cdlemg21  36467  cdlemg33d  36490  dibopelvalN  36924  dibopelval2  36926  dib1dim  36946  dicelval2N  36963  diclspsn  36975  lcdlss  37400  mapd1o  37429  mzpcompact2lem  37816  fz1eqin  37834  rexrabdioph  37860  expdiophlem1  38089  dford4  38097  fnwe2lem2  38122  fgraphopab  38289  ifpidg  38336  rp-fakenanass  38360  rp-fakeinunass  38361  rp-isfinite6  38364  elinintrab  38383  elnonrel  38391  elmapintab  38402  dfrtrcl5  38436  imaiun1  38443  coiun1  38444  rfovcnvf1od  38798  andi3or  38820  uneqsn  38821  ntrneicls00  38887  2sbc5g  39116  pm14.12  39121  2sb5nd  39274  uun2221  39537  uun2221p1  39538  uun2221p2  39539  2sb5ndVD  39640  2sb5ndALT  39662  disjinfi  39869  climuz  40456  dfxlim2  40554  cncfshift  40567  dvnmul  40638  dvnprodlem2  40642  ismbl3  40682  ismbl4  40689  stoweidlem26  40722  stoweidlem35  40731  fourierdlem54  40856  fourierdlem83  40885  fourierdlem100  40902  fourierdlem104  40906  fourierdlem109  40911  fourierdlem112  40914  smfpimcc  41496  reuan  41692  2reu4a  41701  dfdfat2  41717  ffnaov  41788  an4com24  41857  4an21  41859  iccpartiltu  41933  isrnghm  42460  2zrngmmgm  42514  rngcinv  42549  rngcinvALTV  42561  ringcinv  42600  ringcinvALTV  42624  opeliun2xp  42679  pgrpgt2nabl  42715  islindeps  42810  lindslinindsimp1  42814  lindslinindsimp2  42820  ldepslinc  42866  blen1b  42950  dffun3f  42997  setrec1lem3  43004  elpglem3  43027  elpg  43028
  Copyright terms: Public domain W3C validator