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

Theorem anbi1i 731
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 671 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:  anbi2ci  732  anbi12i  733  pm5.53  854  an12  855  anandi  888  dfifp4  1036  dfifp5  1037  3ancoma  1062  3ioran  1073  3an4anass  1314  an6  1448  an3andi  1485  an33rean  1486  19.26-3an  1840  19.28v  1965  19.28  2134  eeeanv  2219  19.28OLD  2271  sb3an  2428  sbel2x  2487  2eu4  2585  r19.26-3  3095  r19.41v  3118  r19.41  3119  rexcomf  3126  3reeanv  3137  rabrab  3146  cbvreu  3199  ceqsex3v  3277  rexab  3402  rexrab  3403  rmo4  3432  reuind  3444  sbc3an  3527  rmo3  3561  ssrab  3713  rexun  3826  elin3  3837  inass  3856  dfun2  3892  indifdir  3916  difin2  3923  inrab2  3933  rabun2  3939  reuun2  3943  undif4  4068  rexdifpr  4238  rexsns  4249  rexdifsn  4356  2ralunsn  4455  iuncom4  4560  iunxiun  4640  disjxun  4683  zfrep4  4812  inuni  4856  reusv2lem4  4902  reusv2  4904  otth2  4981  copsexg  4985  copsex4g  4988  opeqsn  4996  opelopabsbALT  5013  dfid3  5054  wefrc  5137  rabxp  5188  opeliunxp  5204  xpundir  5206  xpiundi  5207  xpiundir  5208  brinxp2  5214  copsex2gb  5263  brresg  5435  brresOLD  5439  dmres  5454  restidsing  5493  restidsingOLD  5494  dminss  5582  imainss  5583  difxp  5593  ssrnres  5607  cnvresima  5661  coundi  5674  resco  5677  imaco  5678  coiun  5683  coi1  5689  coass  5692  cnvpo  5711  xpco  5713  elsnxpOLD  5716  wfi  5751  dffun2  5936  fncnv  6000  imadif  6011  mptun  6063  fcnvres  6120  dff1o2  6180  dff1o3  6181  brprcneu  6222  fvun2  6309  eqfnfv3  6353  respreima  6384  f1ompt  6422  fsn  6442  fmptsng  6475  fmptsnd  6476  tpres  6507  abrexco  6542  imaiun  6543  f1mpt  6558  dff1o6  6571  oprabid  6717  dfoprab2  6743  oprab4  6768  mpt2mptx  6793  resiexg  7144  elxp4  7152  elxp5  7153  ffoss  7169  f11o  7170  opabex3d  7187  opabex3  7188  abexssex  7191  elxp7  7245  dfopab2  7266  dfoprab3s  7267  1stconst  7310  2ndconst  7311  frxp  7332  xporderlem  7333  suppssov1  7372  suppssfv  7376  brtpos2  7403  tpostpos  7417  tposmpt2  7434  wfrfun  7470  dfrecs3  7514  oarec  7687  oeeu  7728  mapsncnv  7946  dfixp  7952  domen  8010  mapsnen  8076  xpsnen  8085  xpcomco  8091  xpassen  8095  sbthlem9  8119  frfi  8246  marypha2lem2  8383  epfrs  8645  tcsni  8657  cp  8792  bnd2  8794  dfac5lem1  8984  dfac5lem2  8985  dfac5lem5  8988  kmlem3  9012  dfackm  9026  cfval2  9120  cflim3  9122  cfss  9125  cfslb  9126  zfcndrep  9474  eltsk2g  9611  ltexpi  9762  recmulnq  9824  ltexprlem4  9899  addsrpr  9934  mulsrpr  9935  addcnsr  9994  mulcnsr  9995  ltresr  9999  axrrecex  10022  elnnz  11425  elnn0z  11428  fnn0ind  11514  rexuz2  11777  rexrp  11891  elixx3g  12226  elfz2  12371  elfzuzb  12374  fznn  12446  elfz2nn0  12469  fznn0  12470  4fvwrd4  12498  preduz  12500  elfzo2  12512  fzind2  12626  hashf1lem1  13277  hashf1lem2  13278  fz1isolem  13283  s4f1o  13709  wwlktovfo  13747  fsum2dlem  14545  modfsummod  14570  sinltx  14963  divalglem10  15172  divalgb  15174  coprmproddvdslem  15423  isprm2  15442  infpn2  15664  prdsle  16169  prdsless  16170  prdsleval  16184  imasleval  16248  dfiso2  16479  oppcsect  16485  elhoma  16729  ispos2  16995  lubeldm  17028  glbeldm  17041  tosso  17083  ismhm  17384  issubm  17394  submacs  17412  issubg  17641  issubg3  17659  gaorb  17786  pmtrrn2  17926  efgcpbllema  18213  efgcpbllemb  18214  frgpuplem  18231  subgdmdprd  18479  dprd2d2  18489  dfrhm2  18765  drngprop  18806  drngid2  18811  opprdrng  18819  issubrg  18828  isabv  18867  islss  18983  islbs  19124  lsmspsn  19132  isassa  19363  aspval2  19395  ltbval  19519  opsrle  19523  opsrtoslem1  19532  isobs  20112  islinds  20196  fvmptnn04if  20702  ntreq0  20929  restntr  21034  cnnei  21134  hausnei2  21205  cmpcov2  21241  cmpsub  21251  uncmp  21254  cmpfi  21259  llyi  21325  subislly  21332  dissnlocfin  21380  iskgen3  21400  1stckgenlem  21404  ptpjpre1  21422  txcnpi  21459  txtube  21491  hausdiag  21496  txlm  21499  txkgen  21503  cfinfil  21744  csdfil  21745  supfil  21746  fin1aufil  21783  elflim2  21815  hauspwpwf1  21838  txflf  21857  isfcls  21860  alexsubALTlem3  21900  alexsubALT  21902  cnextcn  21918  istmd  21925  istgp  21928  tgphaus  21967  qustgplem  21971  istrg  22014  istdrg  22016  istlm  22035  blres  22283  isms2  22302  metrest  22376  metustid  22406  metuel2  22417  restmetu  22422  isngp  22447  isnlm  22526  elii1  22781  isclmp  22943  iscvsp  22974  isncvsngp  22995  iscph  23016  cfilucfil3  23163  isbn  23181  limcrcl  23683  ig1pval3  23979  plydivex  24097  ellogdm  24430  cubic  24621  dmarea  24729  vmasum  24986  lgsquadlem1  25150  lgsquadlem2  25151  istrkg3ld  25405  legov  25525  ltgov  25537  colinearalg  25835  axeuclid  25888  axcontlem2  25890  axcontlem5  25893  nbgrel  26278  nbgrelOLD  26279  nbupgrres  26310  nbusgredgeu0  26314  nb3grprlem2  26327  nb3grpr2  26329  nb3gr2nb  26330  cplgr3v  26387  finsumvtxdg2ssteplem3  26499  wlkonprop  26610  upgrtrls  26654  upgristrl  26655  wksonproplem  26657  usgr2pth0  26717  wlknwwlksnsur  26844  wlkwwlksur  26851  wwlksnext  26856  wwlksnextsur  26863  wwlksnfi  26869  wlksnwwlknvbij  26871  wspthsnwspthsnon  26879  wpthswwlks2on  26927  wpthswwlks2onOLD  26928  rusgrnumwwlkl1  26935  erclwwlkref  26977  isclwwlknx  26998  clwwlknwwlksn  27000  clwwlknwwlksnOLD  27001  erclwwlknref  27033  clwwlknonel  27070  clwwlknon1  27072  clwwlknon2x  27078  clwwlkvbij  27088  clwwlkvbijOLD  27089  iseupthf1o  27180  2pthfrgrrn  27262  fusgr2wsp2nb  27314  numclwlk1lem2f1  27347  numclwwlkovh  27353  numclwlk2lem2f1o  27359  numclwlk2lem2f1oOLD  27366  frgrregord013  27382  avril1  27449  islno  27736  h2hlm  27965  hcau  28169  hhsssh2  28255  dfch2  28394  elcnop  28844  ellnop  28845  elhmop  28860  elcnfn  28869  ellnfn  28870  dmadjss  28874  adjeu  28876  adjval  28877  hhcno  28891  hhcnf  28892  eleigvec  28944  isst  29200  ishst  29201  cvnbtwn3  29275  cvnbtwn4  29276  chirredi  29381  sumdmdii  29402  or3di  29435  spc2ed  29440  rexunirn  29458  rmo3f  29462  rmo4fOLD  29463  difrab2  29465  iunin1f  29500  disjunsn  29533  opeldifid  29538  ofpreima  29593  mpt2mptxf  29605  1stpreima  29612  2ndpreima  29613  f1od2  29627  resf1o  29633  maprnin  29634  nndiffz1  29676  omndmul2  29840  isorng  29927  smatrcl  29990  pcmplfin  30055  ordtconnlem1  30098  isrrext  30172  sigaex  30300  sigaval  30301  isrnsigaOLD  30303  omssubaddlem  30489  omssubadd  30490  eulerpartleme  30553  eulerpartlemt0  30559  eulerpartlemr  30564  eulerpartlemn  30571  probun  30609  ballotlemelo  30677  ballotlem2  30678  ballotlemfc0  30682  ballotlemfcc  30683  reprdifc  30833  bnj248  30894  bnj250  30895  bnj268  30903  bnj312  30906  bnj945  30970  bnj110  31054  bnj849  31121  bnj882  31122  bnj893  31124  bnj916  31129  bnj983  31147  bnj1040  31166  bnj1175  31198  erdszelem1  31299  iscvm  31367  elmpst  31559  mpstrcl  31564  dfso3  31727  coepr  31768  dfpo2  31771  dfdm5  31800  dfrn5  31801  elima4  31803  imaindm  31806  frpoind  31865  frind  31868  soseq  31879  frrlem5c  31911  elno3  31933  slenlt  32002  madeval2  32061  brtxp  32112  brpprod  32117  dfon3  32124  elfix  32135  dffix2  32137  sscoid  32145  elfuns  32147  brimg  32169  brapply  32170  brsuccf  32173  funpartlem  32174  funpartfun  32175  brrestrict  32181  dfrecs2  32182  dfrdg4  32183  lineunray  32379  ellines  32384  finminlem  32437  fneval  32472  neibastop3  32482  bj-inrab  33048  bj-rest10  33166  bj-restpw  33170  bj-restuni  33175  bj-mpt2mptALT  33197  bj-elid3  33217  icorempt2  33329  isbasisrelowllem1  33333  isbasisrelowllem2  33334  relowlpssretop  33342  rabiun  33512  iundif1  33513  lindsenlbs  33534  poimirlem4  33543  poimirlem25  33564  poimirlem26  33565  poimirlem29  33568  poimirlem30  33569  ismblfin  33580  ovoliunnfl  33581  voliunnfl  33583  volsupnfl  33584  itg2addnclem2  33592  itg2addnclem3  33593  itg2addnc  33594  ftc1anc  33623  isbnd2  33712  bndss  33715  heibor1lem  33738  heibor1  33739  isrngohom  33894  isidl  33943  sbccom2lem  34059  anan  34142  eqelb  34145  brinxp2ALTV  34175  eldmqsres  34192  idinxpssinxp2  34230  moantr  34267  inxpxrn  34293  dfcoss3  34312  cocossss  34331  br1cossinidres  34339  br1cossincnvepres  34340  br1cossxrnidres  34341  br1cossxrncnvepres  34342  refrelcoss2  34354  symrelcoss2  34356  cosscnvssid5  34368  br1cossxrncnvssrres  34398  dfrefrel3  34406  dfcnvrefrel3  34419  cosselcnvrefrels2  34424  cosselcnvrefrels3  34425  cosselcnvrefrels4  34426  cosselcnvrefrels5  34427  dfsymrel3  34436  refsymrel2  34451  refsymrel3  34452  elrefsymrels3  34454  prtlem70  34460  prtlem100  34463  prter2  34485  lsateln0  34600  islshpat  34622  lcvnbtwn3  34633  islfl  34665  ishlat1  34957  ishlat2  34958  cvrat4  35047  islvol5  35183  psubspset  35348  snatpsubN  35354  dalawlem13  35487  psubclsetN  35540  isltrn2N  35724  cdlemftr3  36170  dibelval3  36753  dicval2  36785  dicopelval2  36787  dicelval2N  36788  dihglb2  36948  islpolN  37089  lcfls1c  37142  mapdvalc  37235  mapdval4N  37238  mapdordlem1a  37240  elmzpcl  37606  mzpindd  37626  fphpd  37697  pw2f1ocnv  37921  islmodfg  37956  islssfg2  37958  isdomn3  38099  rp-fakeoranass  38176  rp-isfinite6  38181  elmapintrab  38199  elinintrab  38200  relintab  38206  dfrtrcl5  38253  fsovrfovd  38620  ntrk1k3eqk13  38665  gneispace3  38748  k0004lem1  38762  pm13.192  38928  opelopab4  39084  ax6e2nd  39091  en3lplem2VD  39393  ax6e2ndVD  39458  ax6e2ndALT  39480  ssrabf  39612  limcrecl  40179  dvnprodlem2  40480  fourierdlem103  40744  fourierdlem104  40745  4an21  41611  sprvalpwn0  42058  xpsnopab  42090  ismgmhm  42108  issubmgm  42114  submgmacs  42129  sgrp2sgrp  42189  opeliun2xp  42436  mpt2mptx2  42438  lindslinindsimp1  42571  lindslinindsimp2  42577  alsconv  42864  aacllem  42875
  Copyright terms: Public domain W3C validator