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	|- ( ph <-> ps )

Assertion

Ref	Expression
anbi1i	|- ( ( ph /\ ch ) <-> ( ps /\ ch ) )

Proof of Theorem anbi1i

Step	Hyp	Ref	Expression
1		anbi.1	. . 3 |- ( ph <-> ps )
2	1	a1i 11	. 2 |- ( ch -> ( ph <-> ps ) )
3	2	pm5.32ri 670	1 |- ( ( ph /\ ch ) <-> ( ps /\ ch ) )

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:  anbi2ci  732  anbi12i  733  pm5.53  837  an12  838  anandi  871  pm5.75OLD  979  dfifp4  1016  dfifp5  1017  3ancoma  1045  3ioran  1056  3an4anass  1291  an6  1408  an3andi  1445  an33rean  1446  19.26-3an  1800  19.28v  1909  19.28  2096  eeeanv  2183  19.28OLD  2235  sb3an  2400  sbel2x  2459  2eu4  2556  r19.26-3  3066  r19.41v  3089  r19.41  3090  rexcomf  3097  3reeanv  3108  cbvreu  3169  ceqsex3v  3246  rexab  3369  rexrab  3370  rmo4  3399  reuind  3411  sbc3an  3494  rmo3  3528  ssrab  3680  rexun  3793  elin3  3804  inass  3823  dfun2  3859  indifdir  3883  difin2  3890  inrab2  3900  rabun2  3906  reuun2  3910  undif4  4035  rexdifpr  4205  rexsns  4217  rexdifsn  4323  2ralunsn  4423  iuncom4  4528  iunxiun  4608  disjxun  4651  zfrep4  4779  inuni  4826  reusv2lem4  4872  reusv2  4874  otth2  4952  copsexg  4956  copsex4g  4959  opeqsn  4967  opelopabsbALT  4984  dfid3  5025  wefrc  5108  rabxp  5154  opeliunxp  5170  xpundir  5172  xpiundi  5173  xpiundir  5174  brinxp2  5180  copsex2gb  5230  brres  5402  brresg  5405  dmres  5419  restidsing  5458  restidsingOLD  5459  dminss  5547  imainss  5548  difxp  5558  ssrnres  5572  cnvresima  5623  coundi  5636  resco  5639  imaco  5640  coiun  5645  coi1  5651  coass  5654  cnvpo  5673  xpco  5675  elsnxpOLD  5678  wfi  5713  dffun2  5898  fncnv  5962  imadif  5973  mptun  6025  fcnvres  6082  dff1o2  6142  dff1o3  6143  brprcneu  6184  fvun2  6270  eqfnfv3  6313  respreima  6344  f1ompt  6382  fsn  6402  fmptsng  6434  fmptsnd  6435  tpres  6466  abrexco  6502  imaiun  6503  f1mpt  6518  dff1o6  6531  oprabid  6677  dfoprab2  6701  oprab4  6726  mpt2mptx  6751  resiexg  7102  elxp4  7110  elxp5  7111  ffoss  7127  f11o  7128  opabex3d  7145  opabex3  7146  abexssex  7149  elxp7  7201  dfopab2  7222  dfoprab3s  7223  1stconst  7265  2ndconst  7266  frxp  7287  xporderlem  7288  suppssov1  7327  suppssfv  7331  brtpos2  7358  tpostpos  7372  tposmpt2  7389  wfrfun  7425  dfrecs3  7469  oarec  7642  oeeu  7683  mapsncnv  7904  dfixp  7910  domen  7968  mapsnen  8035  xpsnen  8044  xpcomco  8050  xpassen  8054  sbthlem9  8078  frfi  8205  marypha2lem2  8342  epfrs  8607  tcsni  8619  cp  8754  bnd2  8756  dfac5lem1  8946  dfac5lem2  8947  dfac5lem5  8950  kmlem3  8974  dfackm  8988  cfval2  9082  cflim3  9084  cfss  9087  cfslb  9088  zfcndrep  9436  eltsk2g  9573  ltexpi  9724  recmulnq  9786  ltexprlem4  9861  addsrpr  9896  mulsrpr  9897  addcnsr  9956  mulcnsr  9957  ltresr  9961  axrrecex  9984  elnnz  11387  elnn0z  11390  fnn0ind  11476  rexuz2  11739  rexrp  11853  elixx3g  12188  elfz2  12333  elfzuzb  12336  fznn  12408  elfz2nn0  12431  fznn0  12432  4fvwrd4  12459  preduz  12461  elfzo2  12473  fzind2  12586  hashf1lem1  13239  hashf1lem2  13240  fz1isolem  13245  s4f1o  13663  wwlktovfo  13701  fsum2dlem  14501  modfsummod  14526  sinltx  14919  divalglem10  15125  divalgb  15127  coprmproddvdslem  15376  isprm2  15395  infpn2  15617  prdsle  16122  prdsless  16123  prdsleval  16137  imasleval  16201  dfiso2  16432  oppcsect  16438  elhoma  16682  ispos2  16948  lubeldm  16981  glbeldm  16994  tosso  17036  ismhm  17337  issubm  17347  submacs  17365  issubg  17594  issubg3  17612  gaorb  17740  pmtrrn2  17880  efgcpbllema  18167  efgcpbllemb  18168  frgpuplem  18185  subgdmdprd  18433  dprd2d2  18443  dfrhm2  18717  drngprop  18758  drngid2  18763  opprdrng  18771  issubrg  18780  isabv  18819  islss  18935  islbs  19076  lsmspsn  19084  isassa  19315  aspval2  19347  ltbval  19471  opsrle  19475  opsrtoslem1  19484  isobs  20064  islinds  20148  fvmptnn04if  20654  ntreq0  20881  restntr  20986  cnnei  21086  hausnei2  21157  cmpcov2  21193  cmpsub  21203  uncmp  21206  cmpfi  21211  llyi  21277  subislly  21284  dissnlocfin  21332  iskgen3  21352  1stckgenlem  21356  ptpjpre1  21374  txcnpi  21411  txtube  21443  hausdiag  21448  txlm  21451  txkgen  21455  cfinfil  21697  csdfil  21698  supfil  21699  fin1aufil  21736  elflim2  21768  hauspwpwf1  21791  txflf  21810  isfcls  21813  alexsubALTlem3  21853  alexsubALT  21855  cnextcn  21871  istmd  21878  istgp  21881  tgphaus  21920  qustgplem  21924  istrg  21967  istdrg  21969  istlm  21988  blres  22236  isms2  22255  metrest  22329  metustid  22359  metuel2  22370  restmetu  22375  isngp  22400  isnlm  22479  elii1  22734  isclmp  22897  iscvsp  22928  isncvsngp  22949  iscph  22970  cfilucfil3  23117  isbn  23135  limcrcl  23638  ig1pval3  23934  plydivex  24052  ellogdm  24385  cubic  24576  dmarea  24684  vmasum  24941  lgsquadlem1  25105  lgsquadlem2  25106  istrkg3ld  25360  legov  25480  ltgov  25492  colinearalg  25790  axeuclid  25843  axcontlem2  25845  axcontlem5  25848  nbgrel  26238  nbupgrres  26266  nbusgredgeu0  26270  nb3grprlem2  26283  nb3grpr2  26285  nb3gr2nb  26286  cplgr3v  26331  finsumvtxdg2ssteplem3  26443  wlkonprop  26554  upgrtrls  26598  upgristrl  26599  wksonproplem  26601  usgr2pth0  26661  wlknwwlksnsur  26776  wlkwwlksur  26783  wwlksnext  26788  wwlksnextsur  26795  wwlksnfi  26801  wlksnwwlknvbij  26803  wpthswwlks2on  26854  rusgrnumwwlkl1  26863  isclwwlksnx  26889  clwwlksvbij  26922  erclwwlksref  26934  erclwwlksnref  26946  iseupthf1o  27062  2pthfrgrrn  27146  fusgr2wsp2nb  27198  clwwlksnwwlksn  27209  numclwwlkovf2  27217  numclwlk2lem2f1o  27238  frgrregord013  27253  avril1  27319  islno  27608  h2hlm  27837  hcau  28041  hhsssh2  28127  dfch2  28266  elcnop  28716  ellnop  28717  elhmop  28732  elcnfn  28741  ellnfn  28742  dmadjss  28746  adjeu  28748  adjval  28749  hhcno  28763  hhcnf  28764  eleigvec  28816  isst  29072  ishst  29073  cvnbtwn3  29147  cvnbtwn4  29148  chirredi  29253  sumdmdii  29274  or3di  29307  spc2ed  29312  rexunirn  29331  rmo3f  29335  rmo4fOLD  29336  rabrab  29338  difrab2  29339  iunin1f  29374  disjunsn  29407  opeldifid  29412  ofpreima  29465  mpt2mptxf  29477  1stpreima  29484  2ndpreima  29485  f1od2  29499  resf1o  29505  maprnin  29506  nndiffz1  29548  omndmul2  29712  isorng  29799  smatrcl  29862  pcmplfin  29927  ordtconnlem1  29970  isrrext  30044  sigaex  30172  sigaval  30173  isrnsigaOLD  30175  omssubaddlem  30361  omssubadd  30362  eulerpartleme  30425  eulerpartlemt0  30431  eulerpartlemr  30436  eulerpartlemn  30443  probun  30481  ballotlemelo  30549  ballotlem2  30550  ballotlemfc0  30554  ballotlemfcc  30555  reprdifc  30705  bnj248  30766  bnj250  30767  bnj268  30775  bnj312  30778  bnj945  30844  bnj110  30928  bnj849  30995  bnj882  30996  bnj893  30998  bnj916  31003  bnj983  31021  bnj1040  31040  bnj1175  31072  erdszelem1  31173  iscvm  31241  elmpst  31433  mpstrcl  31438  dfso3  31601  coepr  31642  dfpo2  31645  dfdm5  31676  dfrn5  31677  elima4  31679  imaindm  31682  frind  31740  soseq  31751  wzelOLD  31772  frrlem5c  31786  elno3  31808  slenlt  31877  madeval2  31936  brtxp  31987  brpprod  31992  dfon3  31999  elfix  32010  dffix2  32012  sscoid  32020  elfuns  32022  brimg  32044  brapply  32045  brsuccf  32048  funpartlem  32049  funpartfun  32050  brrestrict  32056  dfrecs2  32057  dfrdg4  32058  lineunray  32254  ellines  32259  finminlem  32312  fneval  32347  neibastop3  32357  bj-inrab  32923  bj-rest10  33041  bj-restpw  33045  bj-restuni  33050  bj-mpt2mptALT  33072  bj-elid3  33087  icorempt2  33199  isbasisrelowllem1  33203  isbasisrelowllem2  33204  relowlpssretop  33212  rabiun  33382  iundif1  33383  lindsenlbs  33404  poimirlem4  33413  poimirlem25  33434  poimirlem26  33435  poimirlem29  33438  poimirlem30  33439  ismblfin  33450  ovoliunnfl  33451  voliunnfl  33453  volsupnfl  33454  itg2addnclem2  33462  itg2addnclem3  33463  itg2addnc  33464  ftc1anc  33493  isbnd2  33582  bndss  33585  heibor1lem  33608  heibor1  33609  isrngohom  33764  isidl  33813  sbccom2lem  33929  anan  33999  eqelb  34002  brinxp2ALTV  34034  eldmqsres  34051  idinxpssinxp2  34089  motr  34127  prtlem70  34141  prtlem100  34144  prter2  34166  lsateln0  34282  islshpat  34304  lcvnbtwn3  34315  islfl  34347  ishlat1  34639  ishlat2  34640  cvrat4  34729  islvol5  34865  psubspset  35030  snatpsubN  35036  dalawlem13  35169  psubclsetN  35222  isltrn2N  35406  cdlemftr3  35853  dibelval3  36436  dicval2  36468  dicopelval2  36470  dicelval2N  36471  dihglb2  36631  islpolN  36772  lcfls1c  36825  mapdvalc  36918  mapdval4N  36921  mapdordlem1a  36923  elmzpcl  37289  mzpindd  37309  fphpd  37380  pw2f1ocnv  37604  islmodfg  37639  islssfg2  37641  isdomn3  37782  rp-fakeoranass  37859  rp-isfinite6  37864  elmapintrab  37882  elinintrab  37883  relintab  37889  dfrtrcl5  37936  fsovrfovd  38303  ntrk1k3eqk13  38348  gneispace3  38431  k0004lem1  38445  pm13.192  38611  opelopab4  38767  ax6e2nd  38774  en3lplem2VD  39079  ax6e2ndVD  39144  ax6e2ndALT  39166  ssrabf  39298  limcrecl  39861  dvnprodlem2  40162  fourierdlem103  40426  fourierdlem104  40427  sprvalpwn0  41733  xpsnopab  41765  ismgmhm  41783  issubmgm  41789  submgmacs  41804  sgrp2sgrp  41864  opeliun2xp  42111  mpt2mptx2  42113  lindslinindsimp1  42246  lindslinindsimp2  42252  alsconv  42536  aacllem  42547