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

Theorem anbi2i 624
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 576 1 ((𝜒𝜑) ↔ (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397
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 206  df-an 398
This theorem is referenced by:  anbi1ci  627  anbi12i  628  bianass  641  an42  656  anandir  676  dfbi3  1049  dn1  1057  dfifp3  1065  ifpdfbi  1070  an3andi  1483  an33rean  1484  an33reanOLD  1485  anxordi  1527  cadcoma  1614  nic-mpALT  1675  nic-axALT  1677  3exdistr  1965  4exdistr  1966  19.27v  1994  19.27  2221  19.41  2229  2sb5  2272  dfsb7  2276  dfeumo  2536  mo4f  2566  eu3v  2569  eu6  2573  dfeu  2594  eu2  2610  eu4  2616  2mos  2650  2eu4  2655  ceqsex3v  3501  ceqsex4v  3502  ceqsex8v  3504  reu2  3684  reu6  3685  reu4  3690  reu7  3691  rmo3f  3693  rmo4f  3694  2reu5lem3  3716  2reu5  3717  sbcimdv  3814  sbcg  3819  rmo3  3846  reuan  3853  dfpss2  4046  difdif  4091  raldifb  4105  inass  4180  dfss4  4219  dfin2  4221  indi  4234  indifdi  4244  indifdirOLD  4246  undif3  4251  difin0ss  4329  inssdif0  4330  2nreu  4402  2reu4lem  4484  rexdifpr  4620  reuprg0  4664  ssdifsn  4749  ssunpr  4793  uniprg  4883  uniprOLD  4885  uniun  4892  uniin  4893  csbuni  4898  dfiun2g  4991  iunin2  5032  iundif2  5035  iindif2  5038  iinin2  5039  elpwpw  5063  axrep1  5244  axrep4  5248  reusv2lem4  5357  eqvinop  5445  opcom  5459  fconstmpt  5695  opeliunxp  5700  xpundi  5701  elvvv  5708  opelinxp  5712  xpiindi  5792  elcnv2  5834  cnvuni  5843  dmuni  5871  brres  5945  dmres  5960  elidinxp  5998  restidsing  6007  elima3  6021  asymref  6071  imainss  6107  difxp  6117  xpdifid  6121  mptpreima  6191  coundir  6201  resco  6203  coass  6218  relrelss  6226  opreu2reurex  6247  dfpo2  6249  frpoind  6297  wfiOLD  6306  ordtri3or  6350  dffun2  6507  dffun2OLD  6508  dffun2OLDOLD  6509  dffun6  6510  dffun3  6511  dffun3OLD  6512  dffun4  6513  dffun5  6514  dffun6f  6515  dffun7  6529  dffun8  6530  dffun9  6531  svrelfun  6574  fncnv  6575  imadif  6586  dfmpt3  6636  fcnvres  6720  fint  6722  fin  6723  dff12  6738  fores  6767  dff1o4  6793  eqfnfv3  6985  fndmin  6996  fniniseg  7011  unpreima  7014  ffnfvf  7068  fsn2  7083  tpres  7151  fconstfv  7163  dff13f  7204  dff14a  7218  dff14b  7219  isocnv2  7277  f1opr  7414  eloprabga  7465  ffnov  7484  eqfnov  7486  foov  7529  uniuni  7697  tfindsg  7798  findsg  7837  funcnvuni  7869  opabex3d  7899  opabex3rd  7900  opabex3  7901  1stconst  8033  2ndconst  8034  frxp  8059  soxp  8062  xpord3lem  8082  suppvalbr  8097  suppofssd  8135  suppcoss  8139  mpoxopovel  8152  brtpos  8167  tpostpos  8178  dfsmo2  8294  dfrecs3  8319  dfrecs3OLD  8320  rdglem1  8362  tz7.49  8392  brwitnlem  8454  oeeu  8551  naddasslem2  8640  erinxp  8731  mapsncnv  8832  cbvixp  8853  ixpin  8862  ixpiin  8863  mptelixpg  8874  elixpsn  8876  ixpsnf1o  8877  xpassen  9011  omxpenlem  9018  sbthcl  9040  sbthfilem  9146  wemapsolem  9487  dford2  9557  inf2  9560  zfinf  9576  ttrclselem2  9663  trcl  9665  frind  9687  frr3g  9693  iscard2  9913  leweon  9948  aceq1  10054  dfac3  10058  dfac4  10059  dfac5lem2  10061  dfac5  10065  kmlem3  10089  kmlem4  10090  kmlem14  10100  kmlem15  10101  dfackm  10103  infmap2  10155  fin23lem25  10261  zorn2lem7  10439  brdom6disj  10469  zfcndrep  10551  zfcndinf  10555  fpwwe  10583  axgroth4  10769  grothprim  10771  grothtsk  10772  nqpr  10951  addsrmo  11010  mulsrmo  11011  opelreal  11067  elnnz  12510  elznn0nn  12514  peano2uz2  12592  nnwos  12841  dflt2  13068  xmullem  13184  4fvwrd4  13562  preduz  13564  elfznelfzo  13678  fzind2  13691  fsuppmapnn0fiubex  13898  hashinfxadd  14286  hashgt23el  14325  hashfun  14338  fi1uzind  14397  brfi1uzind  14398  opfi1uzind  14401  cotr2g  14862  shftdm  14957  rexfiuz  15233  cbvsum  15581  mertenslem2  15771  mertens  15772  cbvprod  15799  prodmo  15820  iprodmul  15887  divalglem10  16285  ndvdssub  16292  bitsmod  16317  algcvgblem  16454  isprm2  16559  isprm4  16561  hashdvds  16648  infpn2  16786  hashbc0  16878  xpscf  17448  funcpropd  17788  isffth2  17804  eldmcoa  17952  setcinv  17977  xpccatid  18077  yonedainv  18171  ispos  18204  ispos2  18205  joinfval2  18264  meetfval2  18278  istsr2  18474  isnsg2  18959  isnsg4  18970  isgim  19053  oppgid  19138  oppgcntz  19146  symgfix2  19199  efgval2  19507  iscyg2  19660  dmdprdd  19779  subgdmdprd  19814  issrg  19920  oppr1  20064  opprunit  20091  opprirred  20132  isrhm  20153  subsubrg2  20252  islmim  20526  lbsextg  20626  lidlnz  20701  isdomn2  20772  resubdrg  21015  unocv  21087  pjfval2  21118  islinds2  21222  opsrtoslem1  21465  mdetunilem8  21971  istop2g  22248  isbasis2g  22301  tgval2  22309  isclo2  22442  isnrm2  22712  is1stc2  22796  llyi  22828  isfbas2  23189  elfg  23225  ufinffr  23283  isfcls  23363  alexsubALTlem2  23402  alexsubALTlem3  23403  cnextcn  23421  ustfilxp  23567  iscusp2  23657  metustid  23913  isclmp  24463  iscvsp  24494  tcphcph  24604  iscau3  24645  caucfil  24650  mdegleb  25432  ellogdm  25997  dvdsflsumcom  26540  logfac2  26568  dchrelbas3  26589  dchrvmasumlema  26851  nosupno  27054  noinfno  27069  noinfbnd1lem1  27074  dmscut  27153  made0  27206  legtrid  27536  outpasch  27700  axcontlem5  27920  axcontlem6  27921  axcontlem7  27922  nb3grpr2  28334  iscplgr  28366  pthdlem1  28717  wwlksnextinj  28847  usgr2wspthon  28913  rusgrnumwwlkl1  28916  isclwwlk  28931  clwwlkccatlem  28936  clwwlknon2x  29050  iseupthf1o  29149  frcond3  29216  frgr3v  29222  4cycl2vnunb  29237  frgrncvvdeqlem2  29247  fusgr2wsp2nb  29281  numclwlk1lem1  29316  hhcms  30148  isch3  30186  ocsh  30228  pjhtheu  30339  pjpreeq  30343  h1deoi  30494  h1dei  30495  eleigvec  30902  cvbr2  31228  cvnbtwn2  31232  cvnbtwn4  31234  mdsl2i  31267  cvmdi  31269  mdsymlem6  31353  cdj3lem3b  31385  mo5f  31420  nmo  31421  rexunirn  31423  dmrab  31428  difrab2  31429  disjunsn  31515  unipreima  31563  dfcnv2  31595  1stpreima  31623  lsmsnorb2  32176  prmidl0  32226  ssmxidl  32242  ressply1mon1p  32281  zarcls  32458  rhmpreimacnlem  32468  isrnsiga  32715  rossros  32782  omsmeas  32926  eulerpartlemr  32977  eulerpartlemgvv  32979  ballotlemodife  33100  plymulx  33163  signstfvneq0  33187  bnj251  33317  bnj252  33318  bnj257  33322  bnj290  33325  bnj1304  33434  bnj153  33495  bnj543  33508  bnj571  33521  bnj580  33528  bnj607  33531  bnj882  33541  bnj964  33558  bnj996  33571  bnj1033  33584  bnj1176  33620  bnj1186  33622  bnj1189  33624  bnj1204  33627  bnj1253  33632  bnj1452  33667  bnj1463  33670  dff15  33691  fineqvrep  33699  fineqvac  33701  lfuhgr3  33716  cusgredgex2  33719  usgrgt2cycl  33727  2cycl2d  33736  dfacycgr1  33741  erdszelem9  33796  cvmlift2lem9  33908  cvmlift2lem13  33912  satfvsucsuc  33962  satfdm  33966  satf0  33969  fmlasucdisj  33996  satffunlem  33998  satffunlem1lem1  33999  satffunlem2lem1  34001  elmthm  34173  axinfprim  34280  axacprim  34281  xpab  34300  dfso2  34331  dford5reg  34360  dfon2lem5  34365  dfon2  34370  brtxp2  34469  brpprod3a  34474  dfom5b  34500  brcart  34520  brimg  34525  funpartlem  34530  dfrecs2  34538  cgrxfr  34643  segletr  34702  trer  34791  fneval  34827  neifg  34846  df3nandALT1  34874  andnand1  34876  nandsym1  34897  bj-eu3f  35310  bj-csbsnlem  35373  bj-snsetex  35437  bj-elsngl  35442  bj-snglc  35443  bj-restuni  35571  bj-dfmpoa  35592  bj-imdirco  35664  mptsnunlem  35812  icorempo  35825  isbasisrelowllem2  35830  relowlpssretop  35838  rdgeqoa  35844  difunieq  35848  dffinxpf  35859  nlpineqsn  35882  curf  36059  finixpnum  36066  ptrest  36080  poimirlem1  36082  poimirlem14  36095  poimirlem16  36097  poimirlem19  36100  poimirlem25  36106  poimirlem26  36107  poimirlem27  36108  poimir  36114  cnambfre  36129  itg2addnc  36135  ftc1anc  36162  opropabco  36186  isdrngo1  36418  keridl  36494  ispridlc  36532  selconj  36562  eldmqsres  36750  cnvepres  36762  ecinn0  36817  alrmomorn  36822  moantr  36828  dfxrn2  36841  disjressuc2  36853  inxpxrn  36860  rnxrnres  36864  coss2cnvepres  36883  refrelredund4  37100  dferALTV2  37133  dfeldisj3  37184  dfpart2  37234  prtlem70  37322  prtlem100  37324  prtlem15  37340  islshpat  37482  lcvbr2  37487  lcvbr3  37488  lcvnbtwn2  37492  ellkr  37554  cvrval2  37739  cvrnbtwn2  37740  cvrnbtwn3  37741  cvrnbtwn4  37744  ishlat2  37818  lplnexatN  38029  islvol5  38045  dath  38202  pclfinclN  38416  lhpexle3  38478  4atex2  38543  4atex2-0bOLDN  38545  isltrn2N  38586  cdleme0nex  38756  cdleme22b  38807  cdlemg17pq  39138  cdlemg19  39150  cdlemg21  39152  cdlemg33d  39175  dibopelvalN  39609  dibopelval2  39611  dib1dim  39631  dicelval2N  39648  diclspsn  39660  lcdlss  40085  mapd1o  40114  3factsumint2  40482  3factsumint3  40483  3factsumint  40485  sticksstones16  40573  sticksstones21  40578  metakunt1  40580  mhphf  40774  mzpcompact2lem  41077  fz1eqin  41095  rexrabdioph  41120  expdiophlem1  41348  dford4  41356  fnwe2lem2  41381  fgraphopab  41540  dflim6  41602  onsucf1olem  41608  onsucrn  41609  nnoeomeqom  41649  faosnf0.11b  41706  ifpidg  41770  rp-fakeinunass  41794  rp-isfinite6  41797  dfsucon  41802  elinintrab  41856  elnonrel  41864  elmapintab  41875  dfrtrcl5  41908  imaiun1  41930  coiun1  41931  rfovcnvf1od  42283  andi3or  42303  uneqsn  42304  ntrneicls00  42368  rr-groth  42586  ismnushort  42588  rr-grothshortbi  42590  2sbc5g  42703  pm14.12  42708  2sb5nd  42849  uun2221  43102  uun2221p1  43103  uun2221p2  43104  2sb5ndVD  43199  2sb5ndALT  43221  iindif2f  43382  disjinfi  43419  climuz  43992  dfxlim2  44096  cncfshift  44122  dvnmul  44191  dvnprodlem2  44195  ismbl3  44234  ismbl4  44241  stoweidlem26  44274  stoweidlem35  44283  fourierdlem54  44408  fourierdlem83  44437  fourierdlem100  44454  fourierdlem104  44458  fourierdlem109  44463  fourierdlem112  44466  smfpimcc  45056  fcoresf1ob  45314  f1cof1b  45316  f1ocof1ob  45320  2reu8i  45352  dfdfat2  45367  ffnaov  45438  an4com24  45507  4an21  45509  iccpartiltu  45621  prproropf1olem0  45701  isrnghm  46197  2zrngmmgm  46251  rngcinv  46286  rngcinvALTV  46298  ringcinv  46337  ringcinvALTV  46361  opeliun2xp  46415  pgrpgt2nabl  46449  islindeps  46541  lindslinindsimp1  46545  lindslinindsimp2  46551  ldepslinc  46597  blen1b  46681  i0oii  46959  io1ii  46960  iscnrm3lem3  46975  isthinc2  47049  isthinc3  47050  isthincd2  47065  dffun3f  47134  setrec1lem3  47141  elpglem3  47165  elpg  47166
  Copyright terms: Public domain W3C validator