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

Theorem anbi1i 612
Description: Introduce a right conjunct to both sides of a logical equivalence. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)
Hypothesis
Ref Expression
anbi.1 (𝜑𝜓)
Assertion
Ref Expression
anbi1i ((𝜑𝜒) ↔ (𝜓𝜒))

Proof of Theorem anbi1i
StepHypRef Expression
1 anbi.1 . . 3 (𝜑𝜓)
21a1i 11 . 2 (𝜒 → (𝜑𝜓))
32pm5.32ri 567 1 ((𝜑𝜒) ↔ (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wb 197  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 198  df-an 385
This theorem is referenced by:  anbi2ci  613  anbi12i  614  an21  626  anandi  658  pm5.53  1018  dfifp4  1082  dfifp5  1083  3ancomaOLD  1113  3an4anass  1122  3ioran  1124  an6  1562  an3andi  1599  an33rean  1600  19.26-3an  1961  19.26-3anOLD  1962  19.28v  2088  19.28  2264  eeeanv  2357  19.28OLD  2409  sb3an  2559  sbel2x  2619  2eu4  2718  r19.26-3  3252  r19.41v  3275  r19.41  3276  rexcomf  3283  3reeanv  3294  rabrab  3303  cbvreu  3356  ceqsex3v  3438  rexab  3563  rexrab  3564  rmo4  3595  reuind  3607  sbc3an  3689  rmo3  3721  ssrab  3875  rexun  3990  elin3  4001  inass  4018  rexin  4038  dfun2  4059  indifdir  4083  difin2  4089  inrab2  4099  rabun2  4105  reuun2  4109  undif4  4229  rexdifpr  4397  rexsns  4408  rexdifsn  4513  2ralunsn  4615  iuncom4  4718  iunxiun  4798  disjxun  4840  zfrep4  4971  inuni  5016  reusv2lem4  5068  reusv2  5070  otth2  5139  copsexg  5143  copsex4g  5146  opeqsnOLD  5156  opelopabsbALT  5177  dfid3  5218  wefrc  5303  rabxp  5352  opeliunxp  5368  xpundir  5370  xpiundi  5371  xpiundir  5372  brinxp2  5378  brinxp2OLD  5379  copsex2gb  5429  brresg  5602  brresOLD  5606  dmres  5620  restidsing  5668  dminss  5756  imainss  5757  difxp  5767  ssrnres  5781  cnvresima  5835  coundi  5848  resco  5851  imaco  5852  coiun  5857  coi1  5863  coass  5866  cnvpo  5885  xpco  5887  wfi  5924  dffun2  6109  fncnv  6171  imadif  6182  mptun  6234  fcnvres  6295  dff1o2  6356  dff1o3  6357  brprcneu  6398  fvun2  6489  eqfnfv3  6533  respreima  6564  f1ompt  6601  f1ossf1o  6616  fsn  6623  fmptsng  6657  fmptsnd  6658  tpres  6689  abrexco  6724  imaiun  6725  f1mpt  6740  dff1o6  6753  oprabid  6903  dfoprab2  6929  oprab4  6954  mpt2mptx  6979  resiexg  7330  elxp4  7338  elxp5  7339  ffoss  7355  f11o  7356  opabex3d  7373  opabex3  7374  abexssex  7377  elxp7  7431  dfopab2  7452  dfoprab3s  7453  1stconst  7497  2ndconst  7498  frxp  7519  xporderlem  7520  suppssov1  7560  suppssfv  7564  brtpos2  7591  tpostpos  7605  tposmpt2  7622  wfrfun  7659  dfrecs3  7703  oarec  7877  oeeu  7918  mapsncnv  8139  dfixp  8145  domen  8203  xpsnen  8281  xpcomco  8287  xpassen  8291  sbthlem9  8315  frfi  8442  marypha2lem2  8579  epfrs  8852  tcsni  8864  cp  8999  bnd2  9001  dfac5lem1  9227  dfac5lem2  9228  dfac5lem5  9231  kmlem3  9257  dfackm  9271  cfval2  9365  cflim3  9367  cfss  9370  cfslb  9371  zfcndrep  9719  eltsk2g  9856  ltexpi  10007  recmulnq  10069  ltexprlem4  10144  addsrpr  10179  mulsrpr  10180  addcnsr  10239  mulcnsr  10240  ltresr  10244  axrrecex  10267  elnnz  11651  elnn0z  11654  fnn0ind  11740  rexuz2  11955  rexrp  12065  elixx3g  12404  elfz2  12554  elfzuzb  12557  fznn  12629  elfz2nn0  12652  fznn0  12653  4fvwrd4  12681  preduz  12683  elfzo2  12695  fzind2  12808  hashf1lem1  13454  hashf1lem2  13455  fz1isolem  13460  s4f1o  13885  wwlktovfo  13924  fsum2dlem  14722  modfsummod  14746  sinltx  15137  divalglem10  15343  divalgb  15345  coprmproddvdslem  15592  isprm2  15611  infpn2  15832  prdsle  16325  prdsless  16326  prdsleval  16340  imasleval  16404  dfiso2  16634  oppcsect  16640  elhoma  16884  ispos2  17151  lubeldm  17184  glbeldm  17197  tosso  17239  ismhm  17540  issubm  17550  submacs  17568  issubg  17794  issubg3  17812  gaorb  17939  pmtrrn2  18079  efgcpbllema  18366  efgcpbllemb  18367  frgpuplem  18384  subgdmdprd  18633  dprd2d2  18643  dfrhm2  18919  drngprop  18960  drngid2  18965  opprdrng  18973  issubrg  18982  isabv  19021  islss  19137  islbs  19281  lsmspsn  19289  isassa  19522  aspval2  19554  ltbval  19678  opsrle  19682  opsrtoslem1  19690  isobs  20272  islinds  20356  fvmptnn04if  20865  ntreq0  21093  restntr  21198  cnnei  21298  hausnei2  21369  cmpcov2  21405  cmpsub  21415  uncmp  21418  cmpfi  21423  llyi  21489  subislly  21496  dissnlocfin  21544  iskgen3  21564  1stckgenlem  21568  ptpjpre1  21586  txcnpi  21623  txtube  21655  hausdiag  21660  txlm  21663  txkgen  21667  cfinfil  21908  csdfil  21909  supfil  21910  fin1aufil  21947  elflim2  21979  hauspwpwf1  22002  txflf  22021  isfcls  22024  alexsubALTlem3  22064  alexsubALT  22066  cnextcn  22082  istmd  22089  istgp  22092  tgphaus  22131  qustgplem  22135  istrg  22178  istdrg  22180  istlm  22199  blres  22447  isms2  22466  metrest  22540  metustid  22570  metuel2  22581  restmetu  22586  isngp  22611  isnlm  22690  elii1  22945  isclmp  23107  iscvsp  23138  isncvsngp  23159  iscph  23180  cfilucfil3  23327  isbn  23345  limcrcl  23850  ig1pval3  24146  plydivex  24264  ellogdm  24597  cubic  24788  dmarea  24896  vmasum  25153  lgsquadlem1  25317  lgsquadlem2  25318  istrkg3ld  25572  legov  25692  ltgov  25704  colinearalg  26002  axeuclid  26055  axcontlem2  26057  axcontlem5  26060  nbgrel  26447  nbgrelOLD  26448  nbupgrres  26479  nbusgredgeu0  26484  nb3grprlem2  26497  nb3grpr2  26499  nb3gr2nb  26500  cplgr3v  26557  finsumvtxdg2ssteplem3  26669  wlkonprop  26780  upgrtrls  26824  upgristrl  26825  wksonproplem  26827  usgr2pth0  26887  wlknwwlksnsurOLD  27015  wlkwwlksurOLD  27023  wwlksnext  27028  wwlksnextsur  27035  wwlksnfi  27041  wlksnwwlknvbijOLD  27044  wspthsnwspthsnon  27052  wpthswwlks2on  27100  wpthswwlks2onOLD  27101  rusgrnumwwlkl1  27108  erclwwlkref  27161  isclwwlknx  27182  clwwlknwwlksn  27184  clwwlknwwlksnOLD  27185  erclwwlknref  27218  clwlknf1oclwwlkn  27246  clwwlknonel  27260  clwwlknon1  27263  clwwlknon2x  27269  clwwlkvbij  27280  clwwlkvbijOLDOLD  27281  clwwlkvbijOLD  27282  iseupthf1o  27373  2pthfrgrrn  27455  fusgr2wsp2nb  27507  numclwwlk1lem2f1  27534  numclwwlkovh  27551  numclwlk2lem2f1o  27557  numclwlk2lem2f1oOLD  27564  frgrregord013  27581  avril1  27648  islno  27934  h2hlm  28163  hcau  28367  hhsssh2  28453  dfch2  28592  elcnop  29042  ellnop  29043  elhmop  29058  elcnfn  29067  ellnfn  29068  dmadjss  29072  adjeu  29074  adjval  29075  hhcno  29089  hhcnf  29090  eleigvec  29142  isst  29398  ishst  29399  cvnbtwn3  29473  cvnbtwn4  29474  chirredi  29579  sumdmdii  29600  or3di  29633  spc2ed  29638  rexunirn  29655  rmo3f  29659  rmo4fOLD  29660  difrab2  29662  iunin1f  29697  disjunsn  29730  opeldifid  29735  ofpreima  29790  mpt2mptxf  29802  1stpreima  29809  2ndpreima  29810  f1od2  29824  resf1o  29830  maprnin  29831  nndiffz1  29873  omndmul2  30035  isorng  30122  smatrcl  30185  pcmplfin  30250  ordtconnlem1  30293  isrrext  30367  sigaex  30495  sigaval  30496  isrnsigaOLD  30498  omssubaddlem  30684  omssubadd  30685  eulerpartleme  30748  eulerpartlemt0  30754  eulerpartlemr  30759  eulerpartlemn  30766  probun  30804  ballotlemelo  30872  ballotlem2  30873  ballotlemfc0  30877  ballotlemfcc  30878  reprdifc  31028  bnj248  31089  bnj250  31090  bnj268  31098  bnj312  31101  bnj945  31165  bnj110  31249  bnj849  31316  bnj882  31317  bnj893  31319  bnj916  31324  bnj983  31342  bnj1040  31361  bnj1175  31393  erdszelem1  31494  iscvm  31562  elmpst  31754  mpstrcl  31759  dfso3  31921  coepr  31962  dfpo2  31965  dfdm5  31994  dfrn5  31995  elima4  31997  imaindm  32000  frpoind  32059  frind  32062  soseq  32073  frrlem5c  32105  elno3  32127  slenlt  32196  madeval2  32255  brtxp  32306  brpprod  32311  dfon3  32318  elfix  32329  dffix2  32331  sscoid  32339  elfuns  32341  brimg  32363  brapply  32364  brsuccf  32367  funpartlem  32368  funpartfun  32369  brrestrict  32375  dfrecs2  32376  dfrdg4  32377  lineunray  32573  ellines  32578  finminlem  32631  fneval  32666  neibastop3  32676  bj-inrab  33232  bj-rest10  33350  bj-restpw  33354  bj-restuni  33359  bj-mpt2mptALT  33381  bj-elid3  33401  icorempt2  33513  isbasisrelowllem1  33517  isbasisrelowllem2  33518  relowlpssretop  33526  rabiun  33693  iundif1  33694  lindsenlbs  33715  poimirlem4  33724  poimirlem25  33745  poimirlem26  33746  poimirlem29  33749  poimirlem30  33750  ismblfin  33761  ovoliunnfl  33762  voliunnfl  33764  volsupnfl  33765  itg2addnclem2  33772  itg2addnclem3  33773  itg2addnc  33774  ftc1anc  33803  isbnd2  33891  bndss  33894  heibor1lem  33917  heibor1  33918  isrngohom  34073  isidl  34122  sbccom2lem  34237  anan  34318  eqelb  34321  eldmqsres  34366  idinxpssinxp2  34402  moantr  34438  inxpxrn  34464  dfcoss3  34483  cocossss  34502  br1cossinidres  34510  br1cossincnvepres  34511  br1cossxrnidres  34512  br1cossxrncnvepres  34513  refrelcoss2  34525  symrelcoss2  34527  cosscnvssid5  34539  br1cossxrncnvssrres  34569  dfrefrel3  34577  dfcnvrefrel3  34590  cosselcnvrefrels2  34595  cosselcnvrefrels3  34596  cosselcnvrefrels4  34597  cosselcnvrefrels5  34598  dfsymrel3  34607  refsymrel2  34624  refsymrel3  34625  elrefsymrels3  34627  prtlem70  34633  prtlem100  34636  prter2  34658  lsateln0  34773  islshpat  34795  lcvnbtwn3  34806  islfl  34838  ishlat1  35130  ishlat2  35131  cvrat4  35221  islvol5  35357  psubspset  35522  snatpsubN  35528  dalawlem13  35661  psubclsetN  35714  isltrn2N  35898  cdlemftr3  36344  dibelval3  36926  dicval2  36958  dicopelval2  36960  dicelval2N  36961  dihglb2  37121  islpolN  37262  lcfls1c  37315  mapdvalc  37408  mapdval4N  37411  mapdordlem1a  37413  elmzpcl  37789  mzpindd  37809  fphpd  37880  pw2f1ocnv  38103  islmodfg  38138  islssfg2  38140  isdomn3  38281  rp-fakeoranass  38357  rp-isfinite6  38362  elmapintrab  38380  elinintrab  38381  relintab  38387  dfrtrcl5  38434  fsovrfovd  38801  ntrk1k3eqk13  38846  gneispace3  38929  k0004lem1  38943  pm13.192  39108  opelopab4  39263  ax6e2nd  39270  en3lplem2VD  39571  ax6e2ndVD  39636  ax6e2ndALT  39658  ssrabf  39788  limcrecl  40339  dvnprodlem2  40640  fourierdlem103  40903  fourierdlem104  40904  4an21  41857  sprvalpwn0  42299  xpsnopab  42331  ismgmhm  42349  issubmgm  42355  submgmacs  42370  sgrp2sgrp  42430  opeliun2xp  42677  mpt2mptx2  42679  lindslinindsimp1  42812  lindslinindsimp2  42818  alsconv  43105  aacllem  43116
  Copyright terms: Public domain W3C validator