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

Theorem anbi2i 729
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 668 1 ((𝜒𝜑) ↔ (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 196  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 197  df-an 386
This theorem is referenced by:  anbi12i  732  bianass  841  an4  864  an42  865  anandir  871  dfbi3  993  dfbi3OLD  994  dn1  1007  dfifp3  1014  an3andi  1442  an33rean  1443  anxordi  1476  cadcoma  1548  nic-mpALT  1594  nic-axALT  1596  19.27v  1905  19.41v  1911  3exdistr  1920  4exdistr  1921  19.27  2093  19.41  2101  19.27OLD  2233  sbn  2390  2sb5  2442  eu5  2495  eu3v  2497  eu2  2508  mo4f  2515  eu4  2517  2mos  2551  2eu4  2555  rexbii  3036  ceqsex3v  3236  ceqsex4v  3237  ceqsex8v  3239  reu2  3381  reu6  3382  reu4  3387  reu7  3388  2reu5lem3  3402  2reu5  3403  rmo3  3514  dfpss2  3676  difdif  3720  raldifb  3734  inass  3807  dfss4  3842  dfin2  3844  indi  3855  indifdir  3865  undif3  3870  difin0ss  3926  inssdif0  3927  rexdifpr  4183  ssunpr  4340  unipr  4422  uniun  4429  uniin  4430  csbuni  4439  iunin2  4557  iundif2  4560  iindif2  4562  iinin2  4563  elpwpw  4586  axrep1  4742  axrep4  4745  notzfaus  4810  reusv2lem4  4842  eqvinop  4925  opcom  4935  opeqsn  4937  snopeqop  4939  fconstmpt  5133  opeliunxp  5141  xpundi  5142  elvvv  5149  xpiindi  5227  elcnv2  5270  cnvuni  5279  dmuni  5304  opelres  5371  elima3  5442  imai  5447  imainss  5517  difxp  5527  xpdifid  5531  ssrnres  5541  mptpreima  5597  coundir  5606  rnco  5610  coass  5623  relrelss  5628  wfi  5682  ordtri3or  5724  dffun2  5867  dffun3  5868  dffun4  5869  dffun5  5870  dffun6f  5871  dffun7  5884  dffun8  5885  dffun9  5886  svrelfun  5929  fncnv  5930  imadif  5941  dfmpt3  5981  fint  6051  fin  6052  dff12  6067  fores  6091  dff1o4  6112  eqfnfv3  6279  fndmin  6290  fniniseg  6304  unpreima  6307  ffnfvf  6355  fsn2  6368  tpres  6431  fconstfv  6441  dff13f  6478  dff14a  6492  dff14b  6493  isocnv2  6546  ffnov  6729  eqfnov  6731  foov  6773  uniuni  6935  tfindsg  7022  findsg  7055  funcnvuni  7081  opabex3d  7106  opabex3  7107  frxp  7247  soxp  7250  suppvalbr  7259  mpt2xopovel  7306  brtpos  7321  tpostpos  7332  dfsmo2  7404  dfrecs3  7429  rdglem1  7471  tz7.49  7500  brwitnlem  7547  oeeu  7643  erinxp  7781  mapsncnv  7864  cbvixp  7885  ixpin  7893  ixpiin  7894  mptelixpg  7905  elixpsn  7907  ixpsnf1o  7908  mapsnen  7995  xpassen  8014  omxpenlem  8021  sbthcl  8042  wemapsolem  8415  dford2  8477  inf2  8480  zfinf  8496  trcl  8564  iscard2  8762  leweon  8794  aceq1  8900  dfac3  8904  dfac4  8905  dfac5lem2  8907  dfac5lem3  8908  dfac5  8911  kmlem3  8934  kmlem4  8935  kmlem14  8945  kmlem15  8946  dfackm  8948  infmap2  9000  cf0  9033  fin23lem25  9106  zorn2lem7  9284  brdom6disj  9314  zfcndrep  9396  zfcndinf  9400  fpwwe  9428  axgroth4  9614  grothprim  9616  grothtsk  9617  nqpr  9796  addsrmo  9854  mulsrmo  9855  opelreal  9911  elnnz  11347  elznn0nn  11351  peano2uz2  11425  nnwos  11715  dflt2  11941  xmullem  12053  elfzuzb  12294  4fvwrd4  12416  preduz  12418  elfznelfzo  12530  fzind2  12542  fsuppmapnn0fiubex  12748  hashinfxadd  13130  hashfun  13180  fi1uzind  13234  brfi1uzind  13235  opfi1uzind  13238  fi1uzindOLD  13240  brfi1uzindOLD  13241  opfi1uzindOLD  13244  cotr2g  13665  shftdm  13761  rexfiuz  14037  cbvsum  14375  mertenslem2  14561  mertens  14562  cbvprod  14589  prodmo  14610  iprodmul  14678  divalglem10  15068  ndvdssub  15076  bitsmod  15101  algcvgblem  15233  isprm2  15338  isprm4  15340  hashdvds  15423  infpn2  15560  hashbc0  15652  xpscf  16166  funcpropd  16500  isffth2  16516  eldmcoa  16655  setcinv  16680  xpccatid  16768  yonedainv  16861  ispos  16887  ispos2  16888  joinfval2  16942  meetfval2  16956  istsr2  17158  isnsg2  17564  isnsg4  17577  isgim  17644  oppgid  17726  oppgcntz  17734  symgfix2  17776  efgval2  18077  iscyg2  18224  dmdprdd  18338  subgdmdprd  18373  issrg  18447  oppr1  18574  opprunit  18601  opprirred  18642  isrhm  18661  subsubrg2  18747  islmim  19002  lbsextg  19102  lidlnz  19168  isdomn2  19239  opsrtoslem1  19424  resubdrg  19894  unocv  19964  pjfval2  19993  islinds2  20092  mdetunilem8  20365  fvmptnn04if  20594  istop2g  20641  isbasis2g  20692  tgval2  20700  isclo2  20832  isnrm2  21102  is1stc2  21185  llyi  21217  isfbas2  21579  elfg  21615  ufinffr  21673  isfcls  21753  alexsubALTlem2  21792  alexsubALTlem3  21793  cnextcn  21811  ustfilxp  21956  iscusp2  22046  elcncf1di  22638  isclmp  22837  iscvsp  22868  tchcph  22976  iscau3  23016  caucfil  23021  ellogdm  24319  dvdsflsumcom  24848  logfac2  24876  dchrelbas3  24897  dchrvmasumlema  25123  legtrid  25420  outpasch  25581  axcontlem5  25782  axcontlem6  25783  axcontlem7  25784  nb3grpr2  26206  pthdlem1  26565  wwlksnextinj  26697  usgr2wspthon  26760  rusgrnumwwlkl1  26764  isclwwlks  26781  iseupthf1o  26962  frgr3v  27037  4cycl2vnunb  27052  frgr2wwlkeqm  27088  fusgr2wsp2nb  27090  numclwwlkovf2  27107  numclwwlk3lem  27130  hhcms  27948  isch3  27986  ocsh  28030  pjhtheu  28141  pjpreeq  28145  h1deoi  28296  h1dei  28297  eleigvec  28704  cvbr2  29030  cvnbtwn2  29034  cvnbtwn4  29036  mdsl2i  29069  cvmdi  29071  mdsymlem6  29155  cdj3lem3b  29187  mo5f  29213  nmo  29214  rexunirn  29220  rmo3f  29224  rmo4fOLD  29225  rmo4f  29226  disjunsn  29293  unipreima  29329  dfcnv2  29360  1stpreima  29368  isrnsigaOLD  29998  isrnsiga  29999  rossros  30066  omsmeas  30208  eulerpartlemr  30259  eulerpartlemgvv  30261  ballotlemodife  30382  plymulx  30447  signstfvneq0  30471  bnj251  30528  bnj252  30529  bnj257  30533  bnj290  30536  bnj1304  30651  bnj153  30711  bnj543  30724  bnj571  30737  bnj580  30744  bnj607  30747  bnj882  30757  bnj964  30774  bnj996  30786  bnj1033  30798  bnj1176  30834  bnj1186  30836  bnj1189  30838  bnj1204  30841  bnj1253  30846  bnj1452  30881  bnj1463  30884  erdszelem9  30942  cvmlift2lem9  31054  cvmlift2lem13  31058  elmthm  31234  axinfprim  31344  axacprim  31345  coep  31402  dfso2  31405  fv1stcnv  31435  fv2ndcnv  31436  dford5reg  31441  dfon2lem5  31446  dfon2  31451  trpredmintr  31485  frind  31494  frr3g  31533  brtxp2  31683  brpprod3a  31688  dfom5b  31714  brcart  31734  brimg  31739  funpartlem  31744  dfrecs2  31752  cgrxfr  31857  segletr  31916  trer  32005  fneval  32042  neifg  32061  df3nandALT1  32091  andnand1  32093  nandsym1  32116  bj-dfssb2  32335  bj-axrep1  32484  bj-axrep4  32487  bj-eu3f  32525  bj-cleljustab  32545  bj-csbsnlem  32598  bj-snsetex  32651  bj-elsngl  32656  bj-snglc  32657  bj-restuni  32740  bj-dfmpt2a  32747  mptsnunlem  32856  icorempt2  32870  isbasisrelowllem2  32875  relowlpssretop  32883  rdgeqoa  32889  dffinxpf  32893  curf  33058  finixpnum  33065  ptrest  33079  poimirlem1  33081  poimirlem14  33094  poimirlem16  33096  poimirlem19  33099  poimirlem25  33105  poimirlem26  33106  poimirlem27  33107  poimir  33113  cnambfre  33129  itg2addnc  33135  ftc1anc  33164  opropabco  33189  f1opr  33190  isdrngo1  33426  keridl  33502  ispridlc  33540  selconj  33573  prtlem70  33658  prtlem100  33662  prtlem15  33679  islshpat  33823  lcvbr2  33828  lcvbr3  33829  lcvnbtwn2  33833  ellkr  33895  cvrval2  34080  cvrnbtwn2  34081  cvrnbtwn3  34082  cvrnbtwn4  34085  ishlat2  34159  lplnexatN  34368  islvol5  34384  dath  34541  pmapglb  34575  polval2N  34711  pclfinclN  34755  lhpexle3  34817  4atex2  34882  4atex2-0bOLDN  34884  isltrn2N  34925  cdleme0nex  35096  cdleme22b  35148  cdlemg17pq  35479  cdlemg19  35491  cdlemg21  35493  cdlemg33d  35516  dibopelvalN  35951  dibopelval2  35953  dib1dim  35973  dicelval2N  35990  diclspsn  36002  lcdlss  36427  mapd1o  36456  mzpcompact2lem  36833  fz1eqin  36851  rexrabdioph  36877  expdiophlem1  37107  dford4  37115  fnwe2lem2  37140  fgraphopab  37308  ifpidg  37356  rp-fakenanass  37380  rp-fakeinunass  37381  rp-isfinite6  37384  elinintrab  37403  elnonrel  37411  elmapintab  37422  dfrtrcl5  37456  imaiun1  37463  coiun1  37464  rfovcnvf1od  37819  andi3or  37841  uneqsn  37842  ntrneicls00  37908  2sbc5g  38138  pm14.12  38143  2sb5nd  38297  uun2221  38561  uun2221p1  38562  uun2221p2  38563  2sb5ndVD  38668  2sb5ndALT  38690  disjinfi  38889  cncfshift  39422  dvnmul  39495  dvnprodlem2  39499  ismbl3  39540  ismbl4  39547  stoweidlem26  39580  stoweidlem35  39589  fourierdlem54  39714  fourierdlem83  39743  fourierdlem100  39760  fourierdlem104  39764  fourierdlem109  39769  fourierdlem112  39772  smfpimcc  40351  reuan  40514  2reu4a  40523  dfdfat2  40545  ffnaov  40613  iccpartiltu  40686  isrnghm  41210  2zrngmmgm  41264  rngcinv  41299  rngcinvALTV  41311  ringcinv  41350  ringcinvALTV  41374  opeliun2xp  41429  pgrpgt2nabl  41465  islindeps  41560  lindslinindsimp1  41564  lindslinindsimp2  41570  ldepslinc  41616  blen1b  41704  dffun3f  41751  setrec1lem3  41759  elpglem3  41779  elpg  41780
  Copyright terms: Public domain W3C validator