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

Theorem anbi2i 732
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 672 1 ((𝜒𝜑) ↔ (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383
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 197  df-an 385
This theorem is referenced by:  anbi12i  735  bianass  877  an4  900  an42  901  anandir  907  annotanannotOLD  978  dfbi3  1036  dfbi3OLD  1037  dn1  1046  dfifp3  1053  an3andi  1590  an33rean  1591  anxordi  1624  cadcoma  1696  nic-mpALT  1742  nic-axALT  1744  3exdistr  2031  4exdistr  2032  19.27v  2069  19.41vOLD  2075  19.27  2238  19.41  2246  19.27OLD  2375  sbn  2524  2sb5  2576  eu5  2629  eu3v  2631  eu2  2643  mo4f  2650  eu4  2652  2mos  2686  2eu4  2690  rexbii  3175  ceqsex3v  3382  ceqsex4v  3383  ceqsex8v  3385  reu2  3531  reu6  3532  reu4  3537  reu7  3538  2reu5lem3  3552  2reu5  3553  rmo3  3665  dfpss2  3830  difdif  3875  raldifb  3889  inass  3962  dfss4  3997  dfin2  3999  indi  4012  indifdir  4022  undif3  4027  difin0ss  4085  inssdif0  4086  rexdifpr  4346  ssdifsn  4459  ssunpr  4506  unipr  4597  uniun  4604  uniin  4605  csbuni  4614  iunin2  4732  iundif2  4735  iindif2  4737  iinin2  4738  elpwpw  4761  axrep1  4920  axrep4  4923  notzfaus  4985  reusv2lem4  5017  eqvinop  5099  opcom  5109  opeqsn  5111  snopeqop  5113  fconstmpt  5316  opeliunxp  5323  xpundi  5324  elvvv  5331  xpiindi  5409  elcnv2  5451  cnvuni  5460  dmuni  5485  opelresOLD  5557  elima3  5627  imai  5632  imainss  5702  difxp  5712  xpdifid  5716  ssrnres  5726  mptpreima  5785  coundir  5794  rnco  5798  coass  5811  relrelss  5816  wfi  5870  ordtri3or  5912  dffun2  6055  dffun3  6056  dffun4  6057  dffun5  6058  dffun6f  6059  dffun7  6072  dffun8  6073  dffun9  6074  svrelfun  6118  fncnv  6119  imadif  6130  dfmpt3  6171  fint  6241  fin  6242  dff12  6257  fores  6281  dff1o4  6302  eqfnfv3  6472  fndmin  6483  fniniseg  6497  unpreima  6500  ffnfvf  6548  fsn2  6562  tpres  6626  fconstfv  6636  dff13f  6672  dff14a  6686  dff14b  6687  isocnv2  6740  ffnov  6925  eqfnov  6927  foov  6969  uniuni  7132  tfindsg  7221  findsg  7254  funcnvuni  7280  opabex3d  7306  opabex3  7307  frxp  7451  soxp  7454  suppvalbr  7463  mpt2xopovel  7511  brtpos  7526  tpostpos  7537  dfsmo2  7609  dfrecs3  7634  rdglem1  7676  tz7.49  7705  brwitnlem  7752  oeeu  7848  erinxp  7984  mapsncnv  8066  cbvixp  8087  ixpin  8095  ixpiin  8096  mptelixpg  8107  elixpsn  8109  ixpsnf1o  8110  mapsnen  8196  xpassen  8215  omxpenlem  8222  sbthcl  8243  wemapsolem  8616  dford2  8686  inf2  8689  zfinf  8705  trcl  8773  iscard2  8988  leweon  9020  aceq1  9126  dfac3  9130  dfac4  9131  dfac5lem2  9133  dfac5lem3  9134  dfac5  9137  kmlem3  9162  kmlem4  9163  kmlem14  9173  kmlem15  9174  dfackm  9176  infmap2  9228  cf0  9261  fin23lem25  9334  zorn2lem7  9512  brdom6disj  9542  zfcndrep  9624  zfcndinf  9628  fpwwe  9656  axgroth4  9842  grothprim  9844  grothtsk  9845  nqpr  10024  addsrmo  10082  mulsrmo  10083  opelreal  10139  elnnz  11575  elznn0nn  11579  peano2uz2  11653  nnwos  11944  dflt2  12170  xmullem  12283  elfzuzb  12525  4fvwrd4  12649  preduz  12651  elfznelfzo  12763  fzind2  12776  fsuppmapnn0fiubex  12982  hashinfxadd  13362  hashfun  13412  fi1uzind  13467  brfi1uzind  13468  opfi1uzind  13471  cotr2g  13912  shftdm  14006  rexfiuz  14282  cbvsum  14620  mertenslem2  14812  mertens  14813  cbvprod  14840  prodmo  14861  iprodmul  14929  divalglem10  15323  ndvdssub  15331  bitsmod  15356  algcvgblem  15488  isprm2  15593  isprm4  15595  hashdvds  15678  infpn2  15815  hashbc0  15907  xpscf  16424  funcpropd  16757  isffth2  16773  eldmcoa  16912  setcinv  16937  xpccatid  17025  yonedainv  17118  ispos  17144  ispos2  17145  joinfval2  17199  meetfval2  17213  istsr2  17415  isnsg2  17821  isnsg4  17834  isgim  17901  oppgid  17982  oppgcntz  17990  symgfix2  18032  efgval2  18333  iscyg2  18480  dmdprdd  18594  subgdmdprd  18629  issrg  18703  oppr1  18830  opprunit  18857  opprirred  18898  isrhm  18919  subsubrg2  19005  islmim  19260  lbsextg  19360  lidlnz  19426  isdomn2  19497  opsrtoslem1  19682  resubdrg  20152  unocv  20222  pjfval2  20251  islinds2  20350  mdetunilem8  20623  fvmptnn04if  20852  istop2g  20899  isbasis2g  20950  tgval2  20958  isclo2  21090  isnrm2  21360  is1stc2  21443  llyi  21475  isfbas2  21836  elfg  21872  ufinffr  21930  isfcls  22010  alexsubALTlem2  22049  alexsubALTlem3  22050  cnextcn  22068  ustfilxp  22213  iscusp2  22303  elcncf1di  22895  isclmp  23093  iscvsp  23124  tchcph  23232  iscau3  23272  caucfil  23277  ellogdm  24580  dvdsflsumcom  25109  logfac2  25137  dchrelbas3  25158  dchrvmasumlema  25384  legtrid  25681  outpasch  25842  axcontlem5  26043  axcontlem6  26044  axcontlem7  26045  nb3grpr2  26479  iscplgr  26516  pthdlem1  26868  wwlksnextinj  27013  usgr2wspthon  27083  rusgrnumwwlkl1  27086  isclwwlk  27103  clwwlkccatlem  27108  clwwlknon2x  27247  iseupthf1o  27350  frcond3  27419  frgr3v  27425  4cycl2vnunb  27440  frgrncvvdeqlem2  27450  fusgr2wsp2nb  27484  numclwlk1lem1  27526  numclwwlk3lemOLD  27546  hhcms  28365  isch3  28403  ocsh  28447  pjhtheu  28558  pjpreeq  28562  h1deoi  28713  h1dei  28714  eleigvec  29121  cvbr2  29447  cvnbtwn2  29451  cvnbtwn4  29453  mdsl2i  29486  cvmdi  29488  mdsymlem6  29572  cdj3lem3b  29604  mo5f  29629  nmo  29630  rexunirn  29635  rmo3f  29639  rmo4fOLD  29640  rmo4f  29641  difrab2  29642  disjunsn  29710  unipreima  29751  dfcnv2  29781  1stpreima  29789  isrnsigaOLD  30480  isrnsiga  30481  rossros  30548  omsmeas  30690  eulerpartlemr  30741  eulerpartlemgvv  30743  ballotlemodife  30864  plymulx  30930  signstfvneq0  30954  bnj251  31073  bnj252  31074  bnj257  31078  bnj290  31081  bnj1304  31193  bnj153  31253  bnj543  31266  bnj571  31279  bnj580  31286  bnj607  31289  bnj882  31299  bnj964  31316  bnj996  31328  bnj1033  31340  bnj1176  31376  bnj1186  31378  bnj1189  31380  bnj1204  31383  bnj1253  31388  bnj1452  31423  bnj1463  31426  erdszelem9  31484  cvmlift2lem9  31596  cvmlift2lem13  31600  elmthm  31776  axinfprim  31886  axacprim  31887  coep  31944  dfso2  31947  fv1stcnv  31981  fv2ndcnv  31982  dford5reg  31988  dfon2lem5  31993  dfon2  31998  trpredmintr  32032  frpoind  32042  frind  32045  frr3g  32081  nosupno  32151  dmscut  32220  brtxp2  32290  brpprod3a  32295  dfom5b  32321  brcart  32341  brimg  32346  funpartlem  32351  dfrecs2  32359  cgrxfr  32464  segletr  32523  trer  32612  fneval  32649  neifg  32668  df3nandALT1  32698  andnand1  32700  nandsym1  32723  bj-dfssb2  32942  bj-axrep1  33090  bj-axrep4  33093  bj-eu3f  33131  bj-cleljustab  33149  bj-csbsnlem  33200  bj-snsetex  33253  bj-elsngl  33258  bj-snglc  33259  bj-restuni  33352  bj-ismooredr2  33367  bj-dfmpt2a  33373  mptsnunlem  33492  icorempt2  33506  isbasisrelowllem2  33511  relowlpssretop  33519  rdgeqoa  33525  dffinxpf  33529  curf  33696  finixpnum  33703  ptrest  33717  poimirlem1  33719  poimirlem14  33732  poimirlem16  33734  poimirlem19  33737  poimirlem25  33743  poimirlem26  33744  poimirlem27  33745  poimir  33751  cnambfre  33767  itg2addnc  33773  ftc1anc  33802  opropabco  33827  f1opr  33828  isdrngo1  34064  keridl  34140  ispridlc  34178  selconj  34211  anbi1ci  34318  brresALTV  34352  eldmqsres  34371  cnvepres  34386  opelinxp  34430  ecinn0  34437  alrmomorn  34442  moantr  34446  dfxrn2  34457  inxpxrn  34472  rnxrnres  34476  prtlem70  34641  prtlem100  34644  prtlem15  34660  islshpat  34803  lcvbr2  34808  lcvbr3  34809  lcvnbtwn2  34813  ellkr  34875  cvrval2  35060  cvrnbtwn2  35061  cvrnbtwn3  35062  cvrnbtwn4  35065  ishlat2  35139  lplnexatN  35348  islvol5  35364  dath  35521  pmapglb  35555  polval2N  35691  pclfinclN  35735  lhpexle3  35797  4atex2  35862  4atex2-0bOLDN  35864  isltrn2N  35905  cdleme0nex  36076  cdleme22b  36127  cdlemg17pq  36458  cdlemg19  36470  cdlemg21  36472  cdlemg33d  36495  dibopelvalN  36930  dibopelval2  36932  dib1dim  36952  dicelval2N  36969  diclspsn  36981  lcdlss  37406  mapd1o  37435  mzpcompact2lem  37812  fz1eqin  37830  rexrabdioph  37856  expdiophlem1  38086  dford4  38094  fnwe2lem2  38119  fgraphopab  38286  ifpidg  38334  rp-fakenanass  38358  rp-fakeinunass  38359  rp-isfinite6  38362  elinintrab  38381  elnonrel  38389  elmapintab  38400  dfrtrcl5  38434  imaiun1  38441  coiun1  38442  rfovcnvf1od  38796  andi3or  38818  uneqsn  38819  ntrneicls00  38885  2sbc5g  39115  pm14.12  39120  2sb5nd  39274  uun2221  39538  uun2221p1  39539  uun2221p2  39540  2sb5ndVD  39641  2sb5ndALT  39663  disjinfi  39875  climuz  40475  dfxlim2  40573  cncfshift  40586  dvnmul  40657  dvnprodlem2  40661  ismbl3  40702  ismbl4  40709  stoweidlem26  40742  stoweidlem35  40751  fourierdlem54  40876  fourierdlem83  40905  fourierdlem100  40922  fourierdlem104  40926  fourierdlem109  40931  fourierdlem112  40934  smfpimcc  41516  reuan  41682  2reu4a  41691  dfdfat2  41713  ffnaov  41781  an4com24  41790  4an21  41792  iccpartiltu  41864  isrnghm  42398  2zrngmmgm  42452  rngcinv  42487  rngcinvALTV  42499  ringcinv  42538  ringcinvALTV  42562  opeliun2xp  42617  pgrpgt2nabl  42653  islindeps  42748  lindslinindsimp1  42752  lindslinindsimp2  42758  ldepslinc  42804  blen1b  42888  dffun3f  42935  setrec1lem3  42942  elpglem3  42965  elpg  42966
  Copyright terms: Public domain W3C validator