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

Theorem anbi2i 730
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 670 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  733  bianass  859  an4  882  an42  883  anandir  889  annotanannotOLD  960  dfbi3  1018  dfbi3OLD  1019  dn1  1028  dfifp3  1035  an3andi  1485  an33rean  1486  anxordi  1519  cadcoma  1591  nic-mpALT  1637  nic-axALT  1639  3exdistr  1926  4exdistr  1927  19.27v  1964  19.41vOLD  1970  19.27  2133  19.41  2141  19.27OLD  2270  sbn  2419  2sb5  2471  eu5  2524  eu3v  2526  eu2  2538  mo4f  2545  eu4  2547  2mos  2581  2eu4  2585  rexbii  3070  ceqsex3v  3277  ceqsex4v  3278  ceqsex8v  3280  reu2  3427  reu6  3428  reu4  3433  reu7  3434  2reu5lem3  3448  2reu5  3449  rmo3  3561  dfpss2  3725  difdif  3769  raldifb  3783  inass  3856  dfss4  3891  dfin2  3893  indi  3906  indifdir  3916  undif3  3921  difin0ss  3979  inssdif0  3980  rexdifpr  4238  ssunpr  4397  unipr  4481  uniun  4488  uniin  4489  csbuni  4498  iunin2  4616  iundif2  4619  iindif2  4621  iinin2  4622  elpwpw  4645  axrep1  4805  axrep4  4808  notzfaus  4870  reusv2lem4  4902  eqvinop  4984  opcom  4994  opeqsn  4996  snopeqop  4998  fconstmpt  5197  opeliunxp  5204  xpundi  5205  elvvv  5212  xpiindi  5290  elcnv2  5332  cnvuni  5341  dmuni  5366  opelresOLD  5438  elima3  5508  imai  5513  imainss  5583  difxp  5593  xpdifid  5597  ssrnres  5607  mptpreima  5666  coundir  5675  rnco  5679  coass  5692  relrelss  5697  wfi  5751  ordtri3or  5793  dffun2  5936  dffun3  5937  dffun4  5938  dffun5  5939  dffun6f  5940  dffun7  5953  dffun8  5954  dffun9  5955  svrelfun  5999  fncnv  6000  imadif  6011  dfmpt3  6052  fint  6122  fin  6123  dff12  6138  fores  6162  dff1o4  6183  eqfnfv3  6353  fndmin  6364  fniniseg  6378  unpreima  6381  ffnfvf  6429  fsn2  6443  tpres  6507  fconstfv  6517  dff13f  6553  dff14a  6567  dff14b  6568  isocnv2  6621  ffnov  6806  eqfnov  6808  foov  6850  uniuni  7013  tfindsg  7102  findsg  7135  funcnvuni  7161  opabex3d  7187  opabex3  7188  frxp  7332  soxp  7335  suppvalbr  7344  mpt2xopovel  7391  brtpos  7406  tpostpos  7417  dfsmo2  7489  dfrecs3  7514  rdglem1  7556  tz7.49  7585  brwitnlem  7632  oeeu  7728  erinxp  7864  mapsncnv  7946  cbvixp  7967  ixpin  7975  ixpiin  7976  mptelixpg  7987  elixpsn  7989  ixpsnf1o  7990  mapsnen  8076  xpassen  8095  omxpenlem  8102  sbthcl  8123  wemapsolem  8496  dford2  8555  inf2  8558  zfinf  8574  trcl  8642  iscard2  8840  leweon  8872  aceq1  8978  dfac3  8982  dfac4  8983  dfac5lem2  8985  dfac5lem3  8986  dfac5  8989  kmlem3  9012  kmlem4  9013  kmlem14  9023  kmlem15  9024  dfackm  9026  infmap2  9078  cf0  9111  fin23lem25  9184  zorn2lem7  9362  brdom6disj  9392  zfcndrep  9474  zfcndinf  9478  fpwwe  9506  axgroth4  9692  grothprim  9694  grothtsk  9695  nqpr  9874  addsrmo  9932  mulsrmo  9933  opelreal  9989  elnnz  11425  elznn0nn  11429  peano2uz2  11503  nnwos  11793  dflt2  12019  xmullem  12132  elfzuzb  12374  4fvwrd4  12498  preduz  12500  elfznelfzo  12613  fzind2  12626  fsuppmapnn0fiubex  12832  hashinfxadd  13212  hashfun  13262  fi1uzind  13317  brfi1uzind  13318  opfi1uzind  13321  cotr2g  13761  shftdm  13855  rexfiuz  14131  cbvsum  14469  mertenslem2  14661  mertens  14662  cbvprod  14689  prodmo  14710  iprodmul  14778  divalglem10  15172  ndvdssub  15180  bitsmod  15205  algcvgblem  15337  isprm2  15442  isprm4  15444  hashdvds  15527  infpn2  15664  hashbc0  15756  xpscf  16273  funcpropd  16607  isffth2  16623  eldmcoa  16762  setcinv  16787  xpccatid  16875  yonedainv  16968  ispos  16994  ispos2  16995  joinfval2  17049  meetfval2  17063  istsr2  17265  isnsg2  17671  isnsg4  17684  isgim  17751  oppgid  17832  oppgcntz  17840  symgfix2  17882  efgval2  18183  iscyg2  18330  dmdprdd  18444  subgdmdprd  18479  issrg  18553  oppr1  18680  opprunit  18707  opprirred  18748  isrhm  18769  subsubrg2  18855  islmim  19110  lbsextg  19210  lidlnz  19276  isdomn2  19347  opsrtoslem1  19532  resubdrg  20002  unocv  20072  pjfval2  20101  islinds2  20200  mdetunilem8  20473  fvmptnn04if  20702  istop2g  20749  isbasis2g  20800  tgval2  20808  isclo2  20940  isnrm2  21210  is1stc2  21293  llyi  21325  isfbas2  21686  elfg  21722  ufinffr  21780  isfcls  21860  alexsubALTlem2  21899  alexsubALTlem3  21900  cnextcn  21918  ustfilxp  22063  iscusp2  22153  elcncf1di  22745  isclmp  22943  iscvsp  22974  tchcph  23082  iscau3  23122  caucfil  23127  ellogdm  24430  dvdsflsumcom  24959  logfac2  24987  dchrelbas3  25008  dchrvmasumlema  25234  legtrid  25531  outpasch  25692  axcontlem5  25893  axcontlem6  25894  axcontlem7  25895  nb3grpr2  26329  iscplgr  26366  pthdlem1  26718  wwlksnextinj  26862  usgr2wspthon  26932  rusgrnumwwlkl1  26935  isclwwlk  26952  clwwlknon2x  27078  iseupthf1o  27180  frcond3  27249  frgr3v  27255  4cycl2vnunb  27270  frgrncvvdeqlem2  27280  fusgr2wsp2nb  27314  clwwlkccatlem  27331  numclwwlk3lemOLD  27369  hhcms  28188  isch3  28226  ocsh  28270  pjhtheu  28381  pjpreeq  28385  h1deoi  28536  h1dei  28537  eleigvec  28944  cvbr2  29270  cvnbtwn2  29274  cvnbtwn4  29276  mdsl2i  29309  cvmdi  29311  mdsymlem6  29395  cdj3lem3b  29427  mo5f  29452  nmo  29453  rexunirn  29458  rmo3f  29462  rmo4fOLD  29463  rmo4f  29464  difrab2  29465  disjunsn  29533  unipreima  29574  dfcnv2  29604  1stpreima  29612  isrnsigaOLD  30303  isrnsiga  30304  rossros  30371  omsmeas  30513  eulerpartlemr  30564  eulerpartlemgvv  30566  ballotlemodife  30687  plymulx  30753  signstfvneq0  30777  bnj251  30896  bnj252  30897  bnj257  30901  bnj290  30904  bnj1304  31016  bnj153  31076  bnj543  31089  bnj571  31102  bnj580  31109  bnj607  31112  bnj882  31122  bnj964  31139  bnj996  31151  bnj1033  31163  bnj1176  31199  bnj1186  31201  bnj1189  31203  bnj1204  31206  bnj1253  31211  bnj1452  31246  bnj1463  31249  erdszelem9  31307  cvmlift2lem9  31419  cvmlift2lem13  31423  elmthm  31599  axinfprim  31709  axacprim  31710  coep  31767  dfso2  31770  fv1stcnv  31804  fv2ndcnv  31805  dford5reg  31811  dfon2lem5  31816  dfon2  31821  trpredmintr  31855  frpoind  31865  frind  31868  frr3g  31904  nosupno  31974  dmscut  32043  brtxp2  32113  brpprod3a  32118  dfom5b  32144  brcart  32164  brimg  32169  funpartlem  32174  dfrecs2  32182  cgrxfr  32287  segletr  32346  trer  32435  fneval  32472  neifg  32491  df3nandALT1  32521  andnand1  32523  nandsym1  32546  bj-dfssb2  32765  bj-axrep1  32913  bj-axrep4  32916  bj-eu3f  32954  bj-cleljustab  32972  bj-csbsnlem  33023  bj-snsetex  33076  bj-elsngl  33081  bj-snglc  33082  bj-restuni  33175  bj-ismooredr2  33190  bj-dfmpt2a  33196  mptsnunlem  33315  icorempt2  33329  isbasisrelowllem2  33334  relowlpssretop  33342  rdgeqoa  33348  dffinxpf  33352  curf  33517  finixpnum  33524  ptrest  33538  poimirlem1  33540  poimirlem14  33553  poimirlem16  33555  poimirlem19  33558  poimirlem25  33564  poimirlem26  33565  poimirlem27  33566  poimir  33572  cnambfre  33588  itg2addnc  33594  ftc1anc  33623  opropabco  33648  f1opr  33649  isdrngo1  33885  keridl  33961  ispridlc  33999  selconj  34032  anbi1ci  34139  brresALTV  34173  eldmqsres  34192  cnvepres  34207  opelinxp  34251  ecinn0  34258  alrmomorn  34263  moantr  34267  dfxrn2  34278  inxpxrn  34293  rnxrnres  34297  prtlem70  34460  prtlem100  34463  prtlem15  34479  islshpat  34622  lcvbr2  34627  lcvbr3  34628  lcvnbtwn2  34632  ellkr  34694  cvrval2  34879  cvrnbtwn2  34880  cvrnbtwn3  34881  cvrnbtwn4  34884  ishlat2  34958  lplnexatN  35167  islvol5  35183  dath  35340  pmapglb  35374  polval2N  35510  pclfinclN  35554  lhpexle3  35616  4atex2  35681  4atex2-0bOLDN  35683  isltrn2N  35724  cdleme0nex  35895  cdleme22b  35946  cdlemg17pq  36277  cdlemg19  36289  cdlemg21  36291  cdlemg33d  36314  dibopelvalN  36749  dibopelval2  36751  dib1dim  36771  dicelval2N  36788  diclspsn  36800  lcdlss  37225  mapd1o  37254  mzpcompact2lem  37631  fz1eqin  37649  rexrabdioph  37675  expdiophlem1  37905  dford4  37913  fnwe2lem2  37938  fgraphopab  38105  ifpidg  38153  rp-fakenanass  38177  rp-fakeinunass  38178  rp-isfinite6  38181  elinintrab  38200  elnonrel  38208  elmapintab  38219  dfrtrcl5  38253  imaiun1  38260  coiun1  38261  rfovcnvf1od  38615  andi3or  38637  uneqsn  38638  ntrneicls00  38704  2sbc5g  38934  pm14.12  38939  2sb5nd  39093  uun2221  39357  uun2221p1  39358  uun2221p2  39359  2sb5ndVD  39460  2sb5ndALT  39482  disjinfi  39694  climuz  40294  dfxlim2  40392  cncfshift  40405  dvnmul  40476  dvnprodlem2  40480  ismbl3  40521  ismbl4  40528  stoweidlem26  40561  stoweidlem35  40570  fourierdlem54  40695  fourierdlem83  40724  fourierdlem100  40741  fourierdlem104  40745  fourierdlem109  40750  fourierdlem112  40753  smfpimcc  41335  reuan  41501  2reu4a  41510  dfdfat2  41532  ffnaov  41600  an4com24  41609  4an21  41611  iccpartiltu  41683  isrnghm  42217  2zrngmmgm  42271  rngcinv  42306  rngcinvALTV  42318  ringcinv  42357  ringcinvALTV  42381  opeliun2xp  42436  pgrpgt2nabl  42472  islindeps  42567  lindslinindsimp1  42571  lindslinindsimp2  42577  ldepslinc  42623  blen1b  42707  dffun3f  42754  setrec1lem3  42761  elpglem3  42784  elpg  42785
  Copyright terms: Public domain W3C validator