Theorem anbi2i 622

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

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

Syntax hints:   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  anbi1ci  625  anbi12i  626  bianass  638  an42  653  anandir  673  dfbi3  1042  dn1  1050  dfifp3  1058  an3andi  1474  an33rean  1475  anxordi  1511  norass  1522  cadcoma  1598  nic-mpALT  1658  nic-axALT  1660  3exdistr  1943  4exdistr  1944  19.27v  1977  19.27  2196  19.41  2204  2sb5  2247  dfsb7  2253  dfsb7OLD  2254  sbnOLD  2497  sbnALT  2551  dfeumo  2575  mo4f  2610  mo4fOLD  2611  eu3v  2615  eu6  2619  eu6OLDOLD  2622  dfeu  2642  eu2  2660  eu4  2669  2mos  2706  2eu4  2713  rexbii  3213  ceqsex3v  3491  ceqsex4v  3492  ceqsex8v  3494  reu2  3655  reu6  3656  reu4  3661  reu7  3662  rmo3f  3664  rmo4f  3665  2reu5lem3  3687  2reu5  3688  rmo3  3806  rmo3OLD  3807  reuan  3814  dfpss2  3989  difdif  4034  raldifb  4048  inass  4122  dfss4  4161  dfin2  4163  indi  4176  indifdir  4186  undif3  4191  difin0ss  4254  inssdif0  4255  2nreu  4313  2reu4lem  4385  rexdifpr  4509  reuprg0  4551  ssdifsn  4633  ssunpr  4678  unipr  4764  uniun  4770  uniin  4771  csbuni  4779  iunin2  4898  iundif2  4901  iindif2  4904  iinin2  4905  elpwpw  4929  axrep1  5089  axrep4  5093  notzfausOLD  5161  reusv2lem4  5200  eqvinop  5277  opcom  5289  fconstmpt  5507  opeliunxp  5512  xpundi  5513  elvvv  5520  opelinxp  5524  xpiindi  5599  elcnv2  5641  cnvuni  5650  dmuni  5676  brres  5748  dmres  5763  elidinxp  5799  restidsing  5807  elima3  5820  asymref  5859  imainss  5894  difxp  5904  xpdifid  5908  mptpreima  5974  coundir  5983  resco  5985  coass  6000  relrelss  6006  opreu2reurex  6027  wfi  6063  ordtri3or  6105  dffun2  6242  dffun3  6243  dffun4  6244  dffun5  6245  dffun6f  6246  dffun7  6259  dffun8  6260  dffun9  6261  svrelfun  6303  fncnv  6304  imadif  6315  dfmpt3  6357  fcnvres  6431  fint  6433  fin  6434  dff12  6449  fores  6475  dff1o4  6498  eqfnfv3  6676  fndmin  6687  fniniseg  6702  unpreima  6705  ffnfvf  6753  fsn2  6768  tpres  6837  fconstfv  6848  dff13f  6886  dff14a  6900  dff14b  6901  isocnv2  6954  f1opr  7076  ffnov  7141  eqfnov  7143  foov  7185  uniuni  7348  tfindsg  7438  findsg  7472  funcnvuni  7499  opabex3d  7529  opabex3rd  7530  opabex3  7531  1stconst  7658  2ndconst  7659  frxp  7680  soxp  7683  suppvalbr  7692  suppofssd  7725  mpoxopovel  7744  brtpos  7759  tpostpos  7770  dfsmo2  7843  dfrecs3  7868  rdglem1  7910  tz7.49  7939  brwitnlem  7990  oeeu  8086  erinxp  8228  mapsncnv  8313  cbvixp  8334  ixpin  8342  ixpiin  8343  mptelixpg  8354  elixpsn  8356  ixpsnf1o  8357  xpassen  8465  omxpenlem  8472  sbthcl  8493  wemapsolem  8867  dford2  8936  inf2  8939  zfinf  8955  trcl  9023  iscard2  9258  leweon  9290  aceq1  9396  dfac3  9400  dfac4  9401  dfac5lem2  9403  dfac5  9407  kmlem3  9431  kmlem4  9432  kmlem14  9442  kmlem15  9443  dfackm  9445  infmap2  9493  fin23lem25  9599  zorn2lem7  9777  brdom6disj  9807  zfcndrep  9889  zfcndinf  9893  fpwwe  9921  axgroth4  10107  grothprim  10109  grothtsk  10110  nqpr  10289  addsrmo  10348  mulsrmo  10349  opelreal  10405  elnnz  11845  elznn0nn  11849  peano2uz2  11924  nnwos  12168  dflt2  12395  xmullem  12511  4fvwrd4  12881  preduz  12883  elfznelfzo  12996  fzind2  13009  fsuppmapnn0fiubex  13214  hashinfxadd  13598  hashgt23el  13637  hashfun  13650  fi1uzind  13705  brfi1uzind  13706  opfi1uzind  13709  cotr2g  14174  shftdm  14268  rexfiuz  14545  cbvsum  14889  mertenslem2  15078  mertens  15079  cbvprod  15106  prodmo  15127  iprodmul  15194  divalglem10  15590  ndvdssub  15597  bitsmod  15622  algcvgblem  15754  isprm2  15859  isprm4  15861  hashdvds  15945  infpn2  16082  hashbc0  16174  xpscf  16671  funcpropd  17003  isffth2  17019  eldmcoa  17158  setcinv  17183  xpccatid  17271  yonedainv  17364  ispos  17390  ispos2  17391  joinfval2  17445  meetfval2  17459  istsr2  17661  isnsg2  18067  isnsg4  18080  isgim  18147  oppgid  18229  oppgcntz  18237  symgfix2  18279  efgval2  18581  iscyg2  18728  dmdprdd  18842  subgdmdprd  18877  issrg  18951  oppr1  19078  opprunit  19105  opprirred  19146  isrhm  19167  subsubrg2  19256  islmim  19528  lbsextg  19628  lidlnz  19694  isdomn2  19765  opsrtoslem1  19955  resubdrg  20438  unocv  20510  pjfval2  20539  islinds2  20643  mdetunilem8  20916  istop2g  21192  isbasis2g  21244  tgval2  21252  isclo2  21384  isnrm2  21654  is1stc2  21738  llyi  21770  isfbas2  22131  elfg  22167  ufinffr  22225  isfcls  22305  alexsubALTlem2  22344  alexsubALTlem3  22345  cnextcn  22363  ustfilxp  22508  iscusp2  22598  metustid  22851  isclmp  23388  iscvsp  23419  tcphcph  23527  iscau3  23568  caucfil  23573  ellogdm  24907  dvdsflsumcom  25451  logfac2  25479  dchrelbas3  25500  dchrvmasumlema  25762  legtrid  26063  outpasch  26227  axcontlem5  26441  axcontlem6  26442  axcontlem7  26443  nb3grpr2  26852  iscplgr  26884  pthdlem1  27233  wwlksnextinj  27363  usgr2wspthon  27430  rusgrnumwwlkl1  27433  isclwwlk  27448  clwwlkccatlem  27453  clwwlknon2x  27568  iseupthf1o  27667  frcond3  27736  frgr3v  27742  4cycl2vnunb  27757  frgrncvvdeqlem2  27767  fusgr2wsp2nb  27801  numclwlk1lem1  27836  hhcms  28667  isch3  28705  ocsh  28747  pjhtheu  28858  pjpreeq  28862  h1deoi  29013  h1dei  29014  eleigvec  29421  cvbr2  29747  cvnbtwn2  29751  cvnbtwn4  29753  mdsl2i  29786  cvmdi  29788  mdsymlem6  29872  cdj3lem3b  29904  mo5f  29941  nmo  29942  rexunirn  29944  dmrab  29948  difrab2  29949  disjunsn  30030  unipreima  30077  dfcnv2  30108  1stpreima  30126  isrnsiga  30985  rossros  31052  omsmeas  31194  eulerpartlemr  31245  eulerpartlemgvv  31247  ballotlemodife  31368  plymulx  31431  signstfvneq0  31455  bnj251  31585  bnj252  31586  bnj257  31590  bnj290  31593  bnj1304  31704  bnj153  31764  bnj543  31777  bnj571  31790  bnj580  31797  bnj607  31800  bnj882  31810  bnj964  31827  bnj996  31839  bnj1033  31851  bnj1176  31887  bnj1186  31889  bnj1189  31891  bnj1204  31894  bnj1253  31899  bnj1452  31934  bnj1463  31937  dff15  31963  lfuhgr3  31976  cusgredgex2  31979  usgrgt2cycl  31987  2cycl2d  31996  dfacycgr1  32001  erdszelem9  32056  cvmlift2lem9  32168  cvmlift2lem13  32172  satfvsucsuc  32222  satfdm  32226  satf0  32229  fmlasucdisj  32256  satffunlem  32258  satffunlem1lem1  32259  satffunlem2lem1  32261  elmthm  32433  axinfprim  32542  axacprim  32543  dfso2  32600  dfpo2  32601  dford5reg  32637  dfon2lem5  32642  dfon2  32647  trpredmintr  32681  frpoind  32691  frind  32696  frr3g  32732  nosupno  32814  dmscut  32883  brtxp2  32953  brpprod3a  32958  dfom5b  32984  brcart  33004  brimg  33009  funpartlem  33014  dfrecs2  33022  cgrxfr  33127  segletr  33186  trer  33275  fneval  33311  neifg  33330  df3nandALT1  33358  andnand1  33360  nandsym1  33381  bj-eu3f  33741  bj-csbsnlem  33797  bj-snsetex  33901  bj-elsngl  33906  bj-snglc  33907  bj-restuni  34008  bj-ismooredr2  34023  bj-dfmpoa  34029  mptsnunlem  34171  icorempo  34184  isbasisrelowllem2  34189  relowlpssretop  34197  rdgeqoa  34203  difunieq  34207  dffinxpf  34218  nlpineqsn  34241  wl-dfrabsb  34413  curf  34422  finixpnum  34429  ptrest  34443  poimirlem1  34445  poimirlem14  34458  poimirlem16  34460  poimirlem19  34463  poimirlem25  34469  poimirlem26  34470  poimirlem27  34471  poimir  34477  cnambfre  34492  itg2addnc  34498  ftc1anc  34527  opropabco  34552  isdrngo1  34787  keridl  34863  ispridlc  34901  selconj  34931  eldmqsres  35096  cnvepres  35108  ecinn0  35160  alrmomorn  35165  moantr  35169  dfxrn2  35180  inxpxrn  35195  rnxrnres  35199  refrelredund4  35422  dferALTV2  35454  dfeldisj3  35504  prtlem70  35545  prtlem100  35547  prtlem15  35563  islshpat  35705  lcvbr2  35710  lcvbr3  35711  lcvnbtwn2  35715  ellkr  35777  cvrval2  35962  cvrnbtwn2  35963  cvrnbtwn3  35964  cvrnbtwn4  35967  ishlat2  36041  lplnexatN  36251  islvol5  36267  dath  36424  pmapglb  36458  polval2N  36594  pclfinclN  36638  lhpexle3  36700  4atex2  36765  4atex2-0bOLDN  36767  isltrn2N  36808  cdleme0nex  36978  cdleme22b  37029  cdlemg17pq  37360  cdlemg19  37372  cdlemg21  37374  cdlemg33d  37397  dibopelvalN  37831  dibopelval2  37833  dib1dim  37853  dicelval2N  37870  diclspsn  37882  lcdlss  38307  mapd1o  38336  mzpcompact2lem  38854  fz1eqin  38872  rexrabdioph  38897  expdiophlem1  39124  dford4  39132  fnwe2lem2  39157  fgraphopab  39316  ifpidg  39363  rp-fakeinunass  39387  rp-isfinite6  39390  dfsucon  39395  elinintrab  39443  elnonrel  39451  elmapintab  39462  dfrtrcl5  39495  imaiun1  39502  coiun1  39503  rfovcnvf1od  39856  andi3or  39878  uneqsn  39879  ntrneicls00  39945  rr-groth  40153  2sbc5g  40307  pm14.12  40312  2sb5nd  40454  uun2221  40707  uun2221p1  40708  uun2221p2  40709  2sb5ndVD  40804  2sb5ndALT  40826  disjinfi  41015  climuz  41588  dfxlim2  41692  cncfshift  41720  dvnmul  41791  dvnprodlem2  41795  ismbl3  41835  ismbl4  41842  stoweidlem26  41875  stoweidlem35  41884  fourierdlem54  42009  fourierdlem83  42038  fourierdlem100  42055  fourierdlem104  42059  fourierdlem109  42064  fourierdlem112  42067  smfpimcc  42646  2reu8i  42850  dfdfat2  42865  ffnaov  42936  an4com24  43005  4an21  43007  iccpartiltu  43086  prproropf1olem0  43168  isrnghm  43663  2zrngmmgm  43717  rngcinv  43752  rngcinvALTV  43764  ringcinv  43803  ringcinvALTV  43827  opeliun2xp  43881  pgrpgt2nabl  43916  islindeps  44010  lindslinindsimp1  44014  lindslinindsimp2  44020  ldepslinc  44066  blen1b  44151  dffun3f  44287  setrec1lem3  44294  elpglem3  44317  elpg  44318