Theorem anim2i 618

Description: Introduce conjunct to both sides of an implication. (Contributed by NM, 3-Jan-1993.)

Hypothesis

Ref	Expression
anim1i.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
anim2i	⊢ ((𝜒 ∧ 𝜑) → (𝜒 ∧ 𝜓))

Proof of Theorem anim2i

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜒 → 𝜒)
2		anim1i.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	anim12i 614	1 ⊢ ((𝜒 ∧ 𝜑) → (𝜒 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  sylanr2  681  andi  1004  19.41v  1950  exdistrf  2469  equs45f  2482  sbimiOLD  2515  sbimiALT  2577  moaneu  2708  dariiALT  2751  festinoALT  2760  barocoALT  2762  r19.27v  3184  r19.27vOLD  3185  rspc2ev  3635  reu3  3718  difrab  4277  opthprneg  4795  copsexgw  5381  copsexg  5382  imainss  6011  trssord  6208  ordnbtwn  6281  fof  6590  fv3  6688  fvelimab  6737  dff2  6865  dffo5  6870  foco2  6873  fnsnb  6928  tpres  6963  f13dfv  7031  dff1o6  7032  oprabidw  7187  oprabid  7188  ssoprab2i  7263  ndmovass  7336  ndmovdistr  7337  elovmpt3rab1  7405  tfi  7568  find  7607  releldm2  7742  bropopvvv  7785  bropfvvvvlem  7786  ressuppssdif  7851  supp0cosupp0OLD  7873  imacosuppOLD  7875  omlimcl  8204  odi  8205  ixpf  8484  funsnfsupp  8857  hartogs  9008  card2on  9018  zfreg  9059  epfrs  9173  acni3  9473  dfac2b  9556  cflm  9672  axdc2lem  9870  ac6s  9906  ondomon  9985  axregndlem1  10024  axregnd  10026  eltsk2g  10173  grothpw  10248  grothpwex  10249  grothomex  10251  ltexprlem1  10458  ltexprlem4  10461  recexsrlem  10525  elfzp12  12987  focdmex  13712  hashf1rn  13714  hashdifpr  13777  hashgt23el  13786  hashge2el2dif  13839  ccatsymb  13936  swrdnd0  14019  swrdpfx  14069  pfxpfx  14070  pfxccatin12  14095  cshwidxmod  14165  repswcshw  14174  cshimadifsn  14191  cshimadifsn0  14192  pfxco  14200  wwlktovfo  14322  relexpsucnnl  14391  cau3lem  14714  rlimres  14915  dvdsnegb  15627  dvds2add  15643  dvds2sub  15644  nn0onn  15731  gcd2n0cl  15858  lcmfun  15989  divgcdcoprmex  16010  cncongr1  16011  isfunc  17134  drsdirfi  17548  sgrpidmnd  17916  smndex1iidm  18066  gaid  18429  symg2bas  18521  lmhmlem  19801  abvn0b  20075  prmirredlem  20640  psgndiflemB  20744  matsubgcell  21043  tposmap  21066  mat1dim0  21082  mat1dimid  21083  mat1dimscm  21084  mat1dimmul  21085  dmatmul  21106  dmatcrng  21111  scmatcrng  21130  scmatf1  21140  1marepvsma1  21192  maducoeval2  21249  smadiadetlem3lem0  21274  slesolinv  21289  cramerimplem1  21292  cramerimplem2  21293  1pmatscmul  21310  cpmatacl  21324  cpmatmcllem  21326  cpmatmcl  21327  mat2pmatf1  21337  mat2pmatghm  21338  mat2pmatmul  21339  mat2pmatlin  21343  mat2pmatscmxcl  21348  m2cpmmhm  21353  m2pmfzgsumcl  21356  m2cpmrngiso  21366  decpmatmul  21380  pmatcollpw2lem  21385  monmatcollpw  21387  pmatcollpwfi  21390  pmatcollpw3fi1lem2  21395  pmatcollpwscmatlem1  21397  pmatcollpwscmatlem2  21398  pmatcollpwscmat  21399  pm2mpghm  21424  pm2mpmhmlem2  21427  pm2mp  21433  chmatcl  21436  chmatval  21437  chmaidscmat  21456  chfacfisf  21462  chfacfisfcpmat  21463  chfacfscmulcl  21465  chfacfscmul0  21466  chfacfscmulgsum  21468  chfacfpmmul0  21470  chfacfpmmulgsum  21472  chfacfpmmulgsum2  21473  cayhamlem1  21474  cpmidgsumm2pm  21477  cpmidpmatlem2  21479  cpmadugsumlemB  21482  cpmadugsumlemC  21483  cpmadugsumlemF  21484  cpmadugsumfi  21485  cpmidgsum2  21487  cpmadumatpolylem2  21490  cayhamlem2  21492  chcoeffeqlem  21493  cayleyhamilton0  21497  cayleyhamiltonALT  21499  toponcom  21536  neitr  21788  cnprest  21897  nrmsep2  21964  bwth  22018  2ndcsep  22067  isref  22117  reghaus  22433  isfil2  22464  alexsubALTlem3  22657  cnextcn  22675  lpbl  23113  cmodscmulexp  23726  iscau4  23882  caussi  23900  cmetcusp  23957  ovolicc2lem3  24120  limcresi  24483  elply2  24786  elqaa  24911  aannenlem1  24917  aannenlem2  24918  relogbreexp  25353  cxplogb  25364  bpos1lem  25858  tgjustc1  26261  tgjustc2  26262  axcont  26762  usgrexmplef  27041  subupgr  27069  cplgr3v  27217  cusgrfilem2  27238  usgredgsscusgredg  27241  rusgrprop0  27349  uspgr2wlkeqi  27429  trlontrl  27492  spthonpthon  27532  usgr2wlkspthlem1  27538  usgr2wlkspthlem2  27539  clwlkcompim  27561  clwlkl1loop  27564  wwlksnred  27670  wwlksnfiOLD  27685  clwwlknonwwlknonb  27885  clwwlknun  27891  1pthon2v  27932  frcond1  28045  frcond4  28049  frgrnbnb  28072  clwlknon2num  28147  numclwlk1lem1  28148  numclwlk1lem2  28149  numclwwlkovh  28152  numclwwlk2lem1  28155  numclwlk2lem2f  28156  numclwwlk2  28160  isgrpo  28274  vcz  28352  hvsub4  28814  hvaddsub4  28855  5oalem2  29432  5oalem5  29435  5oalem6  29436  3oalem2  29440  homcl  29523  hoadddi  29580  stle0i  30016  spansncv2  30070  mdsymlem1  30180  cdj3lem1  30211  f1ocnt  30525  gsumle  30725  gsumvsca1  30854  gsumvsca2  30855  crefdf  31112  sxbrsigalem0  31529  dya2icoseg2  31536  eulerpartlemgvv  31634  ballotlemirc  31789  bnj168  32000  bnj546  32168  bnj594  32184  bnj1097  32253  bnj1110  32254  bnj1174  32275  bnj1176  32277  cusgredgex2  32369  acycgrislfgr  32399  umgracycusgr  32401  cusgracyclt3v  32403  satfv1  32610  satf0suclem  32622  fmlasuc0  32631  fmlafvel  32632  satffunlem2lem1  32651  satfun  32658  fv1stcnv  33020  noetalem5  33221  colineardim1  33522  idinside  33545  finminlem  33666  ivthALT  33683  lukshef-ax2  33763  bj-19.41al  33992  bj-equs45fv  34133  bj-rest10b  34383  copsex2b  34435  bj-elid6  34465  bj-ccinftydisj  34498  mptsnunlem  34622  topdifinffinlem  34631  relowlssretop  34647  elxp8  34655  fvineqsnf1  34694  pibt1  34700  matunitlindflem1  34903  poimirlem22  34929  poimirlem25  34932  poimirlem27  34934  poimirlem31  34938  ovoliunnfl  34949  itg2addnclem  34958  sstotbnd3  35069  heibor1lem  35102  heibor1  35103  rngmgmbs4  35224  exmid2  35392  redundss3  35878  redundpim3  35880  dalem53  36876  dalem54  36877  linepsubN  36903  pmapsub  36919  elpaddri  36953  pclfinN  37051  pclcmpatN  37052  cdlemg33c0  37853  dihatexv2  38490  eldioph4i  39429  acongtr  39595  pwfi2f1o  39716  aaitgo  39782  frege54cor0a  40229  clsf2  40496  dvsconst  40682  mptssid  41531  xlimxrre  42132  icccncfext  42190  stoweidlem17  42322  elaa2  42539  dmfcoafv  43394  elfzelfzlble  43541  prprelprb  43699  fmtnoprmfac1  43747  fmtnoprmfac2  43749  flsqrt  43776  lighneallem3  43792  proththd  43799  evenprm2  43899  gbogbow  43941  uspgrsprfo  44043  c0mgm  44200  c0rhm  44203  rhmisrnghm  44211  lidlmmgm  44216  2zrngnmrid  44241  rhmsubcrngclem1  44318  srhmsubclem1  44364  rhmsubcALTVlem3  44397  linccl  44489  lincvalpr  44493  lincdifsn  44499  lincext1  44529  lindslinindsimp1  44532  ldepspr  44548  lincresunit3lem1  44554  logblt1b  44644  dignnld  44683  dig1  44688  dignn0flhalflem1  44695  line  44739  rrxline  44741  rrxsphere  44755  itschlc0xyqsol1  44773  itsclc0xyqsolr  44776  amgmwlem  44923