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

Theorem anbi2i 622
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 575 1 ((𝜒𝜑) ↔ (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 207  wa 396
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 208  df-an 397
This theorem is referenced by:  anbi1ci  625  anbi12i  626  bianass  638  an42  653  anandir  673  dfbi3  1041  dn1  1049  dfifp3  1057  an3andi  1473  an33rean  1474  anxordi  1510  norassOLD  1525  cadcoma  1604  nic-mpALT  1664  nic-axALT  1666  3exdistr  1953  4exdistr  1954  19.27v  1987  19.27  2220  19.41  2228  2sb5  2274  dfsb7  2277  dfsb7OLD  2278  sbnOLD  2537  sbnALT  2591  dfeumo  2615  mo4f  2647  eu3v  2651  eu6  2655  dfeu  2677  eu2  2689  eu4  2695  2mos  2730  2eu4  2737  rexbii  3247  ceqsex3v  3546  ceqsex4v  3547  ceqsex8v  3549  reu2  3715  reu6  3716  reu4  3721  reu7  3722  rmo3f  3724  rmo4f  3725  2reu5lem3  3747  2reu5  3748  rmo3  3871  rmo3OLD  3872  reuan  3879  dfpss2  4061  difdif  4106  raldifb  4120  inass  4195  dfss4  4234  dfin2  4236  indi  4249  indifdir  4259  undif3  4264  difin0ss  4327  inssdif0  4328  2nreu  4391  2reu4lem  4463  rexdifpr  4590  reuprg0  4632  ssdifsn  4714  ssunpr  4759  unipr  4845  uniun  4851  uniin  4852  csbuni  4860  iunin2  4985  iundif2  4988  iindif2  4991  iinin2  4992  elpwpw  5016  axrep1  5183  axrep4  5187  notzfausOLD  5255  reusv2lem4  5293  eqvinop  5370  opcom  5383  fconstmpt  5608  opeliunxp  5613  xpundi  5614  elvvv  5621  opelinxp  5625  xpiindi  5700  elcnv2  5742  cnvuni  5751  dmuni  5777  brres  5854  dmres  5869  elidinxp  5905  restidsing  5916  elima3  5930  asymref  5970  imainss  6005  difxp  6015  xpdifid  6019  mptpreima  6086  coundir  6095  resco  6097  coass  6112  relrelss  6118  opreu2reurex  6139  wfi  6175  ordtri3or  6217  dffun2  6359  dffun3  6360  dffun4  6361  dffun5  6362  dffun6f  6363  dffun7  6376  dffun8  6377  dffun9  6378  svrelfun  6420  fncnv  6421  imadif  6432  dfmpt3  6476  fcnvres  6550  fint  6552  fin  6553  dff12  6568  fores  6594  dff1o4  6617  eqfnfv3  6797  fndmin  6808  fniniseg  6823  unpreima  6826  ffnfvf  6876  fsn2  6891  tpres  6956  fconstfv  6967  dff13f  7005  dff14a  7019  dff14b  7020  isocnv2  7073  f1opr  7199  ffnov  7267  eqfnov  7269  foov  7311  uniuni  7472  tfindsg  7563  findsg  7597  funcnvuni  7624  opabex3d  7657  opabex3rd  7658  opabex3  7659  1stconst  7786  2ndconst  7787  frxp  7811  soxp  7814  suppvalbr  7825  suppofssd  7858  mpoxopovel  7877  brtpos  7892  tpostpos  7903  dfsmo2  7975  dfrecs3  8000  rdglem1  8042  tz7.49  8072  brwitnlem  8123  oeeu  8219  erinxp  8361  mapsncnv  8446  cbvixp  8467  ixpin  8476  ixpiin  8477  mptelixpg  8488  elixpsn  8490  ixpsnf1o  8491  xpassen  8600  omxpenlem  8607  sbthcl  8628  wemapsolem  9003  dford2  9072  inf2  9075  zfinf  9091  trcl  9159  iscard2  9394  leweon  9426  aceq1  9532  dfac3  9536  dfac4  9537  dfac5lem2  9539  dfac5  9543  kmlem3  9567  kmlem4  9568  kmlem14  9578  kmlem15  9579  dfackm  9581  infmap2  9629  fin23lem25  9735  zorn2lem7  9913  brdom6disj  9943  zfcndrep  10025  zfcndinf  10029  fpwwe  10057  axgroth4  10243  grothprim  10245  grothtsk  10246  nqpr  10425  addsrmo  10484  mulsrmo  10485  opelreal  10541  elnnz  11980  elznn0nn  11984  peano2uz2  12059  nnwos  12304  dflt2  12531  xmullem  12647  4fvwrd4  13017  preduz  13019  elfznelfzo  13132  fzind2  13145  fsuppmapnn0fiubex  13350  hashinfxadd  13736  hashgt23el  13775  hashfun  13788  fi1uzind  13845  brfi1uzind  13846  opfi1uzind  13849  cotr2g  14326  shftdm  14420  rexfiuz  14697  cbvsum  15042  mertenslem2  15231  mertens  15232  cbvprod  15259  prodmo  15280  iprodmul  15347  divalglem10  15743  ndvdssub  15750  bitsmod  15775  algcvgblem  15911  isprm2  16016  isprm4  16018  hashdvds  16102  infpn2  16239  hashbc0  16331  xpscf  16828  funcpropd  17160  isffth2  17176  eldmcoa  17315  setcinv  17340  xpccatid  17428  yonedainv  17521  ispos  17547  ispos2  17548  joinfval2  17602  meetfval2  17616  istsr2  17818  isnsg2  18248  isnsg4  18259  isgim  18342  oppgid  18424  oppgcntz  18432  symgfix2  18475  efgval2  18781  iscyg2  18932  dmdprdd  19052  subgdmdprd  19087  issrg  19188  oppr1  19315  opprunit  19342  opprirred  19383  isrhm  19404  subsubrg2  19493  islmim  19765  lbsextg  19865  lidlnz  19931  isdomn2  20002  opsrtoslem1  20194  resubdrg  20682  unocv  20754  pjfval2  20783  islinds2  20887  mdetunilem8  21158  istop2g  21434  isbasis2g  21486  tgval2  21494  isclo2  21626  isnrm2  21896  is1stc2  21980  llyi  22012  isfbas2  22373  elfg  22409  ufinffr  22467  isfcls  22547  alexsubALTlem2  22586  alexsubALTlem3  22587  cnextcn  22605  ustfilxp  22750  iscusp2  22840  metustid  23093  isclmp  23630  iscvsp  23661  tcphcph  23769  iscau3  23810  caucfil  23815  ellogdm  25149  dvdsflsumcom  25693  logfac2  25721  dchrelbas3  25742  dchrvmasumlema  26004  legtrid  26305  outpasch  26469  axcontlem5  26682  axcontlem6  26683  axcontlem7  26684  nb3grpr2  27093  iscplgr  27125  pthdlem1  27475  wwlksnextinj  27605  usgr2wspthon  27672  rusgrnumwwlkl1  27675  isclwwlk  27690  clwwlkccatlem  27695  clwwlknon2x  27810  iseupthf1o  27909  frcond3  27976  frgr3v  27982  4cycl2vnunb  27997  frgrncvvdeqlem2  28007  fusgr2wsp2nb  28041  numclwlk1lem1  28076  hhcms  28908  isch3  28946  ocsh  28988  pjhtheu  29099  pjpreeq  29103  h1deoi  29254  h1dei  29255  eleigvec  29662  cvbr2  29988  cvnbtwn2  29992  cvnbtwn4  29994  mdsl2i  30027  cvmdi  30029  mdsymlem6  30113  cdj3lem3b  30145  mo5f  30181  nmo  30182  rexunirn  30184  dmrab  30188  difrab2  30189  disjunsn  30273  unipreima  30320  dfcnv2  30351  1stpreima  30369  isrnsiga  31272  rossros  31339  omsmeas  31481  eulerpartlemr  31532  eulerpartlemgvv  31534  ballotlemodife  31655  plymulx  31718  signstfvneq0  31742  bnj251  31872  bnj252  31873  bnj257  31877  bnj290  31880  bnj1304  31991  bnj153  32052  bnj543  32065  bnj571  32078  bnj580  32085  bnj607  32088  bnj882  32098  bnj964  32115  bnj996  32127  bnj1033  32139  bnj1176  32175  bnj1186  32177  bnj1189  32179  bnj1204  32182  bnj1253  32187  bnj1452  32222  bnj1463  32225  dff15  32251  lfuhgr3  32264  cusgredgex2  32267  usgrgt2cycl  32275  2cycl2d  32284  dfacycgr1  32289  erdszelem9  32344  cvmlift2lem9  32456  cvmlift2lem13  32460  satfvsucsuc  32510  satfdm  32514  satf0  32517  fmlasucdisj  32544  satffunlem  32546  satffunlem1lem1  32547  satffunlem2lem1  32549  elmthm  32721  axinfprim  32830  axacprim  32831  dfso2  32888  dfpo2  32889  dford5reg  32925  dfon2lem5  32930  dfon2  32935  trpredmintr  32968  frpoind  32978  frind  32983  frr3g  33019  nosupno  33101  dmscut  33170  brtxp2  33240  brpprod3a  33245  dfom5b  33271  brcart  33291  brimg  33296  funpartlem  33301  dfrecs2  33309  cgrxfr  33414  segletr  33473  trer  33562  fneval  33598  neifg  33617  df3nandALT1  33645  andnand1  33647  nandsym1  33668  bj-eu3f  34063  bj-csbsnlem  34118  bj-snsetex  34173  bj-elsngl  34178  bj-snglc  34179  bj-restuni  34283  bj-dfmpoa  34303  bj-isrvec  34464  mptsnunlem  34502  icorempo  34515  isbasisrelowllem2  34520  relowlpssretop  34528  rdgeqoa  34534  difunieq  34538  dffinxpf  34549  nlpineqsn  34572  wl-dfrabsb  34743  curf  34752  finixpnum  34759  ptrest  34773  poimirlem1  34775  poimirlem14  34788  poimirlem16  34790  poimirlem19  34793  poimirlem25  34799  poimirlem26  34800  poimirlem27  34801  poimir  34807  cnambfre  34822  itg2addnc  34828  ftc1anc  34857  opropabco  34882  isdrngo1  35117  keridl  35193  ispridlc  35231  selconj  35261  eldmqsres  35426  cnvepres  35438  ecinn0  35490  alrmomorn  35495  moantr  35499  dfxrn2  35510  inxpxrn  35525  rnxrnres  35529  refrelredund4  35752  dferALTV2  35784  dfeldisj3  35834  prtlem70  35875  prtlem100  35877  prtlem15  35893  islshpat  36035  lcvbr2  36040  lcvbr3  36041  lcvnbtwn2  36045  ellkr  36107  cvrval2  36292  cvrnbtwn2  36293  cvrnbtwn3  36294  cvrnbtwn4  36297  ishlat2  36371  lplnexatN  36581  islvol5  36597  dath  36754  pclfinclN  36968  lhpexle3  37030  4atex2  37095  4atex2-0bOLDN  37097  isltrn2N  37138  cdleme0nex  37308  cdleme22b  37359  cdlemg17pq  37690  cdlemg19  37702  cdlemg21  37704  cdlemg33d  37727  dibopelvalN  38161  dibopelval2  38163  dib1dim  38183  dicelval2N  38200  diclspsn  38212  lcdlss  38637  mapd1o  38666  mzpcompact2lem  39228  fz1eqin  39246  rexrabdioph  39271  expdiophlem1  39498  dford4  39506  fnwe2lem2  39531  fgraphopab  39690  ifpidg  39737  rp-fakeinunass  39761  rp-isfinite6  39764  dfsucon  39769  elinintrab  39817  elnonrel  39825  elmapintab  39836  dfrtrcl5  39869  imaiun1  39876  coiun1  39877  rfovcnvf1od  40230  andi3or  40252  uneqsn  40253  ntrneicls00  40319  rr-groth  40515  2sbc5g  40628  pm14.12  40633  2sb5nd  40774  uun2221  41027  uun2221p1  41028  uun2221p2  41029  2sb5ndVD  41124  2sb5ndALT  41146  disjinfi  41334  climuz  41905  dfxlim2  42009  cncfshift  42037  dvnmul  42108  dvnprodlem2  42112  ismbl3  42152  ismbl4  42159  stoweidlem26  42192  stoweidlem35  42201  fourierdlem54  42326  fourierdlem83  42355  fourierdlem100  42372  fourierdlem104  42376  fourierdlem109  42381  fourierdlem112  42384  smfpimcc  42963  2reu8i  43193  dfdfat2  43208  ffnaov  43279  an4com24  43348  4an21  43350  iccpartiltu  43429  prproropf1olem0  43511  isrnghm  44061  2zrngmmgm  44115  rngcinv  44150  rngcinvALTV  44162  ringcinv  44201  ringcinvALTV  44225  opeliun2xp  44279  pgrpgt2nabl  44312  islindeps  44406  lindslinindsimp1  44410  lindslinindsimp2  44416  ldepslinc  44462  blen1b  44546  dffun3f  44683  setrec1lem3  44690  elpglem3  44713  elpg  44714
  Copyright terms: Public domain W3C validator