Theorem anim2i 619

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 615	1 ⊢ ((𝜒 ∧ 𝜑) → (𝜒 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  sylanr2  682  andi  1005  19.41v  1950  exdistrf  2458  equs45f  2471  sbimiALT  2553  moaneu  2685  dariiALT  2728  festinoALT  2737  barocoALT  2739  r19.27v  3151  rspc2ev  3583  reu3  3666  difrab  4229  opthprneg  4755  copsexgw  5346  copsexg  5347  imainss  5978  trssord  6176  ordnbtwn  6249  fof  6565  fv3  6663  fvelimab  6712  dff2  6842  dffo5  6847  foco2  6850  fnsnb  6905  tpres  6940  f13dfv  7009  dff1o6  7010  oprabidw  7166  oprabid  7167  ssoprab2i  7242  ndmovass  7316  ndmovdistr  7317  elovmpt3rab1  7385  tfi  7548  find  7587  findOLD  7588  releldm2  7724  bropopvvv  7768  bropfvvvvlem  7769  ressuppssdif  7834  supp0cosupp0OLD  7856  imacosuppOLD  7858  omlimcl  8187  odi  8188  ixpf  8467  funsnfsupp  8841  hartogs  8992  card2on  9002  zfreg  9043  epfrs  9157  acni3  9458  dfac2b  9541  cflm  9661  axdc2lem  9859  ac6s  9895  ondomon  9974  axregndlem1  10013  axregnd  10015  eltsk2g  10162  grothpw  10237  grothpwex  10238  grothomex  10240  ltexprlem1  10447  ltexprlem4  10450  recexsrlem  10514  elfzp12  12981  focdmex  13707  hashf1rn  13709  hashdifpr  13772  hashgt23el  13781  hashge2el2dif  13834  ccatsymb  13927  swrdnd0  14010  swrdpfx  14060  pfxpfx  14061  pfxccatin12  14086  cshwidxmod  14156  repswcshw  14165  cshimadifsn  14182  cshimadifsn0  14183  pfxco  14191  wwlktovfo  14313  relexpsucnnl  14381  cau3lem  14706  rlimres  14907  dvdsnegb  15619  dvds2add  15635  dvds2sub  15636  nn0onn  15721  gcd2n0cl  15848  lcmfun  15979  divgcdcoprmex  16000  cncongr1  16001  isfunc  17126  drsdirfi  17540  sgrpidmnd  17908  smndex1iidm  18058  gaid  18421  symg2bas  18513  lmhmlem  19794  abvn0b  20068  prmirredlem  20186  psgndiflemB  20289  matsubgcell  21039  tposmap  21062  mat1dim0  21078  mat1dimid  21079  mat1dimscm  21080  mat1dimmul  21081  dmatmul  21102  dmatcrng  21107  scmatcrng  21126  scmatf1  21136  1marepvsma1  21188  maducoeval2  21245  smadiadetlem3lem0  21270  slesolinv  21285  cramerimplem1  21288  cramerimplem2  21289  1pmatscmul  21307  cpmatacl  21321  cpmatmcllem  21323  cpmatmcl  21324  mat2pmatf1  21334  mat2pmatghm  21335  mat2pmatmul  21336  mat2pmatlin  21340  mat2pmatscmxcl  21345  m2cpmmhm  21350  m2pmfzgsumcl  21353  m2cpmrngiso  21363  decpmatmul  21377  pmatcollpw2lem  21382  monmatcollpw  21384  pmatcollpwfi  21387  pmatcollpw3fi1lem2  21392  pmatcollpwscmatlem1  21394  pmatcollpwscmatlem2  21395  pmatcollpwscmat  21396  pm2mpghm  21421  pm2mpmhmlem2  21424  pm2mp  21430  chmatcl  21433  chmatval  21434  chmaidscmat  21453  chfacfisf  21459  chfacfisfcpmat  21460  chfacfscmulcl  21462  chfacfscmul0  21463  chfacfscmulgsum  21465  chfacfpmmul0  21467  chfacfpmmulgsum  21469  chfacfpmmulgsum2  21470  cayhamlem1  21471  cpmidgsumm2pm  21474  cpmidpmatlem2  21476  cpmadugsumlemB  21479  cpmadugsumlemC  21480  cpmadugsumlemF  21481  cpmadugsumfi  21482  cpmidgsum2  21484  cpmadumatpolylem2  21487  cayhamlem2  21489  chcoeffeqlem  21490  cayleyhamilton0  21494  cayleyhamiltonALT  21496  toponcom  21533  neitr  21785  cnprest  21894  nrmsep2  21961  bwth  22015  2ndcsep  22064  isref  22114  reghaus  22430  isfil2  22461  alexsubALTlem3  22654  cnextcn  22672  lpbl  23110  cmodscmulexp  23727  iscau4  23883  caussi  23901  cmetcusp  23958  ovolicc2lem3  24123  limcresi  24488  elply2  24793  elqaa  24918  aannenlem1  24924  aannenlem2  24925  relogbreexp  25361  cxplogb  25372  bpos1lem  25866  tgjustc1  26269  tgjustc2  26270  axcont  26770  usgrexmplef  27049  subupgr  27077  cplgr3v  27225  cusgrfilem2  27246  usgredgsscusgredg  27249  rusgrprop0  27357  uspgr2wlkeqi  27437  trlontrl  27500  spthonpthon  27540  usgr2wlkspthlem1  27546  usgr2wlkspthlem2  27547  clwlkcompim  27569  clwlkl1loop  27572  wwlksnred  27678  clwwlknonwwlknonb  27891  clwwlknun  27897  1pthon2v  27938  frcond1  28051  frcond4  28055  frgrnbnb  28078  clwlknon2num  28153  numclwlk1lem1  28154  numclwlk1lem2  28155  numclwwlkovh  28158  numclwwlk2lem1  28161  numclwlk2lem2f  28162  numclwwlk2  28166  isgrpo  28280  vcz  28358  hvsub4  28820  hvaddsub4  28861  5oalem2  29438  5oalem5  29441  5oalem6  29442  3oalem2  29446  homcl  29529  hoadddi  29586  stle0i  30022  spansncv2  30076  mdsymlem1  30186  cdj3lem1  30217  f1ocnt  30551  gsumle  30775  gsumvsca1  30904  gsumvsca2  30905  crefdf  31201  sxbrsigalem0  31639  dya2icoseg2  31646  eulerpartlemgvv  31744  ballotlemirc  31899  bnj168  32110  bnj546  32278  bnj594  32294  bnj1097  32363  bnj1110  32364  bnj1174  32385  bnj1176  32387  cusgredgex2  32482  acycgrislfgr  32512  umgracycusgr  32514  cusgracyclt3v  32516  satfv1  32723  satf0suclem  32735  fmlasuc0  32744  fmlafvel  32745  satffunlem2lem1  32764  satfun  32771  fv1stcnv  33133  noetalem5  33334  colineardim1  33635  idinside  33658  finminlem  33779  ivthALT  33796  lukshef-ax2  33876  bj-19.41al  34105  bj-equs45fv  34248  bj-rest10b  34504  copsex2b  34555  bj-elid6  34585  bj-ccinftydisj  34628  mptsnunlem  34755  topdifinffinlem  34764  relowlssretop  34780  elxp8  34788  fvineqsnf1  34827  pibt1  34833  matunitlindflem1  35053  poimirlem22  35079  poimirlem25  35082  poimirlem27  35084  poimirlem31  35088  ovoliunnfl  35099  itg2addnclem  35108  sstotbnd3  35214  heibor1lem  35247  heibor1  35248  rngmgmbs4  35369  exmid2  35537  redundss3  36023  redundpim3  36025  dalem53  37021  dalem54  37022  linepsubN  37048  pmapsub  37064  elpaddri  37098  pclfinN  37196  pclcmpatN  37197  cdlemg33c0  37998  dihatexv2  38635  eldioph4i  39753  acongtr  39919  pwfi2f1o  40040  aaitgo  40106  frege54cor0a  40564  clsf2  40829  dvsconst  41034  mptssid  41877  xlimxrre  42473  icccncfext  42529  stoweidlem17  42659  elaa2  42876  dmfcoafv  43731  elfzelfzlble  43878  prprelprb  44034  fmtnoprmfac1  44082  fmtnoprmfac2  44084  flsqrt  44110  lighneallem3  44125  proththd  44132  evenprm2  44232  gbogbow  44274  uspgrsprfo  44376  c0mgm  44533  c0rhm  44536  rhmisrnghm  44544  lidlmmgm  44549  2zrngnmrid  44574  rhmsubcrngclem1  44651  srhmsubclem1  44697  rhmsubcALTVlem3  44730  linccl  44823  lincvalpr  44827  lincdifsn  44833  lincext1  44863  lindslinindsimp1  44866  ldepspr  44882  lincresunit3lem1  44888  logblt1b  44978  dignnld  45017  dig1  45022  dignn0flhalflem1  45029  itcovalsucov  45082  line  45146  rrxline  45148  rrxsphere  45162  itschlc0xyqsol1  45180  itsclc0xyqsolr  45183  amgmwlem  45330