Theorem anbi1i 727

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

Step	Hyp	Ref	Expression
1		anbi.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	a1i 11	. 2 ⊢ (𝜒 → (𝜑 ↔ 𝜓))
3	2	pm5.32ri 668	1 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒))

Syntax hints:   ↔ wb 195   ∧ 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 196  df-an 385

This theorem is referenced by:  anbi2ci  728  anbi12i  729  pm5.53  833  an12  834  anandi  867  pm5.75OLD  975  dfifp4  1010  dfifp5  1011  3ancoma  1038  3ioran  1049  3an4anass  1283  an6  1400  an3andi  1437  an33rean  1438  19.26-3an  1788  19.28v  1896  19.28  2083  eeeanv  2171  19.28OLD  2223  sb3an  2388  sbel2x  2447  2eu4  2544  r19.26-3  3048  r19.41v  3070  r19.41  3071  rexcomf  3078  3reeanv  3087  cbvreu  3145  ceqsex3v  3219  rexab  3336  rexrab  3337  rmo4  3366  reuind  3378  sbc3an  3461  rmo3  3494  ssrab  3643  rexun  3755  elin3  3766  inass  3785  dfun2  3821  indifdir  3842  difin2  3849  inrab2  3859  rabun2  3865  reuun2  3869  undif4  3987  rexsns  4164  rexdifsn  4264  2ralunsn  4361  iuncom4  4464  iunxiun  4544  disjxun  4581  zfrep4  4707  inuni  4753  reusv2lem4  4798  reusv2  4800  otth2  4878  copsexg  4882  copsex4g  4885  opeqsn  4892  opelopabsbALT  4909  dfid3  4954  wefrc  5032  rabxp  5078  opeliunxp  5093  xpundir  5095  xpiundi  5096  xpiundir  5097  brinxp2  5103  copsex2gb  5153  brres  5323  brresg  5325  dmres  5339  restidsing  5377  restidsingOLD  5378  dminss  5466  imainss  5467  difxp  5477  ssrnres  5491  cnvresima  5541  coundi  5553  resco  5556  imaco  5557  coiun  5562  coi1  5568  coass  5571  cnvpo  5590  xpco  5592  elsnxpOLD  5595  wfi  5630  dffun2  5814  fncnv  5876  imadif  5887  mptun  5938  fcnvres  5995  dff1o2  6055  dff1o3  6056  brprcneu  6096  fvun2  6180  eqfnfv3  6221  respreima  6252  f1ompt  6290  fsn  6308  fmptsng  6339  fmptsnd  6340  tpres  6371  abrexco  6406  imaiun  6407  f1mpt  6419  dff1o6  6431  oprabid  6576  dfoprab2  6599  oprab4  6624  mpt2mptx  6649  resiexg  6994  elxp4  7003  elxp5  7004  ffoss  7020  f11o  7021  opabex3d  7037  opabex3  7038  abexssex  7041  elxp7  7092  dfopab2  7113  dfoprab3s  7114  1stconst  7152  2ndconst  7153  frxp  7174  xporderlem  7175  suppssov1  7214  suppssfv  7218  brtpos2  7245  tpostpos  7259  tposmpt2  7276  wfrfun  7312  dfrecs3  7356  oarec  7529  oeeu  7570  mapsncnv  7790  dfixp  7796  domen  7854  mapsnen  7920  xpsnen  7929  xpcomco  7935  xpassen  7939  sbthlem9  7963  frfi  8090  marypha2lem2  8225  epfrs  8490  tcsni  8502  cp  8637  bnd2  8639  dfac5lem1  8829  dfac5lem2  8830  dfac5lem5  8833  kmlem3  8857  dfackm  8871  cfval2  8965  cflim3  8967  cfss  8970  cfslb  8971  zfcndrep  9315  eltsk2g  9452  ltexpi  9603  recmulnq  9665  ltexprlem4  9740  addsrpr  9775  mulsrpr  9776  addcnsr  9835  mulcnsr  9836  ltresr  9840  axrrecex  9863  elnnz  11264  elnn0z  11267  fnn0ind  11352  rexuz2  11615  rexrp  11729  elixx3g  12059  elfz2  12204  elfzuzb  12207  fznn  12278  elfz2nn0  12300  fznn0  12301  4fvwrd4  12328  preduz  12330  elfzo2  12342  fzind2  12448  hashf1lem1  13096  hashf1lem2  13097  fz1isolem  13102  s4f1o  13513  wwlktovfo  13549  fsum2dlem  14343  modfsummod  14367  sinltx  14758  divalglem10  14963  divalgb  14965  coprmproddvdslem  15214  isprm2  15233  infpn2  15455  prdsle  15945  prdsless  15946  prdsleval  15960  imasleval  16024  dfiso2  16255  oppcsect  16261  elhoma  16505  ispos2  16771  lubeldm  16804  glbeldm  16817  tosso  16859  ismhm  17160  issubm  17170  submacs  17188  issubg  17417  issubg3  17435  gaorb  17563  pmtrrn2  17703  efgcpbllema  17990  efgcpbllemb  17991  frgpuplem  18008  subgdmdprd  18256  dprd2d2  18266  dfrhm2  18540  drngprop  18581  drngid2  18586  opprdrng  18594  issubrg  18603  isabv  18642  islss  18756  islbs  18897  lsmspsn  18905  isassa  19136  aspval2  19168  ltbval  19292  opsrle  19296  opsrtoslem1  19305  isobs  19883  islinds  19967  fvmptnn04if  20473  ntreq0  20691  restntr  20796  cnnei  20896  hausnei2  20967  cmpcov2  21003  cmpsub  21013  uncmp  21016  cmpfi  21021  llyi  21087  subislly  21094  dissnlocfin  21142  iskgen3  21162  1stckgenlem  21166  ptpjpre1  21184  txcnpi  21221  txtube  21253  hausdiag  21258  txlm  21261  txkgen  21265  cfinfil  21507  csdfil  21508  supfil  21509  fin1aufil  21546  elflim2  21578  hauspwpwf1  21601  txflf  21620  isfcls  21623  alexsubALTlem3  21663  alexsubALT  21665  cnextcn  21681  istmd  21688  istgp  21691  tgphaus  21730  qustgplem  21734  istrg  21777  istdrg  21779  istlm  21798  blres  22046  isms2  22065  metrest  22139  metustid  22169  metuel2  22180  restmetu  22185  isngp  22210  isnlm  22289  elii1  22542  isclmp  22705  iscvsp  22736  isncvsngp  22757  iscph  22778  cfilucfil3  22925  isbn  22943  limcrcl  23444  ig1pval3  23738  plydivex  23856  ellogdm  24185  cubic  24376  dmarea  24484  vmasum  24741  lgsquadlem1  24905  lgsquadlem2  24906  istrkg3ld  25160  legov  25280  ltgov  25292  colinearalg  25590  axeuclid  25643  axcontlem2  25645  axcontlem5  25648  nb3graprlem2  25981  nb3grapr  25982  nb3grapr2  25983  nb3gra2nb  25984  cusgra2v  25991  trls  26066  3v3e3cycl2  26192  wwlknprop  26214  wlknwwlknsur  26240  wlkiswwlksur  26247  wwlkextsur  26259  wwlknfi  26266  wlknwwlknvbij  26268  clwwlkvbij  26329  erclwwlkref  26341  erclwwlknref  26353  usg2spthonot0  26416  vdgrun  26428  vdgrfiun  26429  2pthfrgrarn  26536  frgrareg  26644  frgraregord013  26645  avril1  26711  islno  26992  h2hlm  27221  hcau  27425  hhsssh2  27511  dfch2  27650  elcnop  28100  ellnop  28101  elhmop  28116  elcnfn  28125  ellnfn  28126  dmadjss  28130  adjeu  28132  adjval  28133  hhcno  28147  hhcnf  28148  eleigvec  28200  isst  28456  ishst  28457  cvnbtwn3  28531  cvnbtwn4  28532  chirredi  28637  sumdmdii  28658  or3di  28691  spc2ed  28696  rexunirn  28715  rmo3f  28719  rmo4fOLD  28720  rabrab  28722  iunin1f  28757  iunxsngf  28758  disjunsn  28789  opeldifid  28794  ofpreima  28848  mpt2mptxf  28860  1stpreima  28867  2ndpreima  28868  f1od2  28887  resf1o  28893  maprnin  28894  nndiffz1  28936  omndmul2  29043  isorng  29130  smatrcl  29190  pcmplfin  29255  ordtconlem1  29298  isrrext  29372  sigaex  29499  sigaval  29500  isrnsigaOLD  29502  omssubaddlem  29688  omssubadd  29689  eulerpartleme  29752  eulerpartlemt0  29758  eulerpartlemr  29763  eulerpartlemn  29770  probun  29808  ballotlemelo  29876  ballotlem2  29877  ballotlemfc0  29881  ballotlemfcc  29882  bnj248  30019  bnj250  30020  bnj268  30028  bnj312  30031  bnj945  30098  bnj110  30182  bnj849  30249  bnj882  30250  bnj893  30252  bnj916  30257  bnj983  30275  bnj1040  30294  bnj1175  30326  erdszelem1  30427  iscvm  30495  elmpst  30687  mpstrcl  30692  dfso3  30856  coepr  30895  dfpo2  30898  dfdm5  30921  dfrn5  30922  elima4  30924  frind  30984  soseq  30995  wzelOLD  31016  frrlem5c  31030  elno3  31052  nofulllem5  31105  brtxp  31157  brpprod  31162  dfon3  31169  elfix  31180  dffix2  31182  sscoid  31190  elfuns  31192  brimg  31214  brapply  31215  brsuccf  31218  funpartlem  31219  funpartfun  31220  brrestrict  31226  dfrecs2  31227  dfrdg4  31228  lineunray  31424  ellines  31429  finminlem  31482  fneval  31517  neibastop3  31527  bj-inrab  32115  bj-rest10  32222  bj-restpw  32226  bj-restuni  32231  bj-mpt2mptALT  32253  bj-elid3  32264  icorempt2  32375  isbasisrelowllem1  32379  isbasisrelowllem2  32380  relowlpssretop  32388  rabiun  32552  iundif1  32553  lindsenlbs  32574  poimirlem4  32583  poimirlem25  32604  poimirlem26  32605  poimirlem29  32608  poimirlem30  32609  ismblfin  32620  ovoliunnfl  32621  voliunnfl  32623  volsupnfl  32624  itg2addnclem2  32632  itg2addnclem3  32633  itg2addnc  32634  ftc1anc  32663  isbnd2  32752  bndss  32755  heibor1lem  32778  heibor1  32779  isrngohom  32934  isidl  32983  sbccom2lem  33099  prtlem70  33157  prtlem100  33161  prter2  33184  lsateln0  33300  islshpat  33322  lcvnbtwn3  33333  islfl  33365  ishlat1  33657  ishlat2  33658  cvrat4  33747  islvol5  33883  psubspset  34048  snatpsubN  34054  dalawlem13  34187  psubclsetN  34240  isltrn2N  34424  cdlemftr3  34871  dibelval3  35454  dicval2  35486  dicopelval2  35488  dicelval2N  35489  dihglb2  35649  islpolN  35790  lcfls1c  35843  mapdvalc  35936  mapdval4N  35939  mapdordlem1a  35941  elmzpcl  36307  mzpindd  36327  fphpd  36398  pw2f1ocnv  36622  islmodfg  36657  islssfg2  36659  isdomn3  36801  rp-fakeoranass  36878  rp-isfinite6  36883  elmapintrab  36901  elinintrab  36902  relintab  36908  dfrtrcl5  36955  fsovrfovd  37323  ntrk1k3eqk13  37368  gneispace3  37451  k0004lem1  37465  pm13.192  37633  opelopab4  37788  ax6e2nd  37795  en3lplem2VD  38101  ax6e2ndVD  38166  ax6e2ndALT  38188  ssrabf  38329  limcrecl  38696  dvnprodlem2  38837  fourierdlem103  39102  fourierdlem104  39103  rexdifpr  40315  nbgrel  40564  nbupgrres  40592  nbusgredgeu0  40596  nb3grprlem2  40609  nb3grpr2  40611  nb3gr2nb  40612  cplgr3v  40657  wlkOnprop  40866  upgrtrls  40909  upgristrl  40910  1wlksonproplem  40912  usgr2pth0  40971  wlknwwlksnsur  41087  wlkwwlksur  41094  wwlksnext  41099  wwlksnextsur  41106  wwlksnfi  41112  wlksnwwlknvbij  41114  wpthswwlks2on  41164  rusgrnumwwlkl1  41172  isclwwlksnx  41197  clwwlksvbij  41229  erclwwlksref  41241  erclwwlksnref  41253  2pthfrgrrn  41452  fusgr2wsp2nb  41498  av-numclwwlkovf2  41515  av-numclwlk2lem2f1o  41535  av-frgraregord013  41549  xpsnopab  41555  ismgmhm  41573  issubmgm  41579  submgmacs  41594  sgrp2sgrp  41654  opeliun2xp  41904  mpt2mptx2  41906  lindslinindsimp1  42040  lindslinindsimp2  42046  alsconv  42345  aacllem  42356