Theorem anim2i 629

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 23	. 2 ⊢ (𝜒 → 𝜒)
2		anim1i.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	anim12i 625	1 ⊢ ((𝜒 ∧ 𝜑) → (𝜒 ∧ 𝜓))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  sylanr2  696  abab  840  andi  1025  19.41v  1981  exdistrf  2476  equs45f  2488  moaneu  2648  dariiALT  2690  festinoALT  2699  barocoALT  2701  r19.27v  3191  reu3  3684  difrab  4263  opthprneg  4819  copsexgwOLD  5460  copsexg  5461  imainss  6143  trssord  6379  ordnbtwn  6458  fof  6796  fv3  6903  fvelimab  6957  dff2  7099  dffo5  7104  foco2  7109  fnsnbOLD  7171  tpres  7207  f13dfv  7282  dff1o6  7283  oprabidw  7451  oprabid  7452  ssoprab2i  7531  ndmovass  7609  ndmovdistr  7610  elovmpt3rab1  7681  tfi  7864  find  7907  releldm2  8054  bropopvvv  8101  bropfvvvvlem  8102  ressuppssdif  8205  omlimcl  8589  odi  8590  ixpf  8951  dif1en  9180  domtrfil  9210  funsnfsupp  9387  hartogs  9541  card2on  9551  zfreg  9593  epfrs  9735  hfuni  9927  acni3  10129  dfac2b  10212  cflm  10330  axdc2lem  10529  ac6s  10565  ondomon  10650  axregndlem1  10690  axregnd  10692  eltsk2g  10839  grothpw  10914  grothpwex  10915  grothomex  10917  ltexprlem1  11124  ltexprlem4  11127  recexsrlem  11191  elfzp12  13740  hashf1rn  14499  hashdifpr  14563  hashgt23el  14572  hashge2el2dif  14628  ccatsymb  14731  swrdnd0  14811  swrdpfx  14860  pfxpfx  14861  pfxccatin12  14886  cshwidxmod  14958  repswcshw  14967  cshimadifsn  14984  cshimadifsn0  14985  pfxco  14993  wwlktovfo  15116  relexpsucnnl  15188  cau3lem  15527  rlimres  15730  dvdsnegb  16448  dvds2add  16465  dvds2sub  16466  nn0onn  16555  gcd2n0cl  16684  lcmfun  16825  divgcdcoprmex  16846  cncongr1  16847  isfunc  18044  drsdirfi  18484  chnrev  18806  sgrpidmnd  18933  smndex1iidm  19102  gaid  19518  symg2bas  19612  qusecsub  20054  gsumle  20364  c0mgm  20694  rhmisrnghm  20716  c0rhm  20791  rhmsubcrngclem1  20923  srhmsubclem1  20934  abvn0b  21098  lmhmlem  21309  unichnlidl  21521  prmirredlem  21783  psgndiflemB  21911  ismhp  22466  matsubgcell  22754  tposmap  22777  mat1dim0  22793  mat1dimid  22794  mat1dimscm  22795  mat1dimmul  22796  dmatmul  22817  dmatcrng  22822  scmatcrng  22841  scmatf1  22851  1marepvsma1  22903  maducoeval2  22960  smadiadetlem3lem0  22985  matunitlindflem1  22999  slesolinv  23003  cramerimplem1  23006  cramerimplem2  23007  1pmatscmul  23025  cpmatacl  23039  cpmatmcllem  23041  cpmatmcl  23042  mat2pmatf1  23052  mat2pmatghm  23053  mat2pmatmul  23054  mat2pmatlin  23058  mat2pmatscmxcl  23063  m2cpmmhm  23068  m2pmfzgsumcl  23071  decpmatmul  23095  pmatcollpw2lem  23100  monmatcollpw  23102  pmatcollpwfi  23105  pmatcollpw3fi1lem2  23110  pmatcollpwscmatlem1  23112  pmatcollpwscmatlem2  23113  pmatcollpwscmat  23114  pm2mpghm  23139  pm2mpmhmlem2  23142  pm2mp  23148  chmatcl  23151  chmatval  23152  chmaidscmat  23171  chfacfisf  23177  chfacfisfcpmat  23178  chfacfscmulcl  23180  chfacfscmul0  23181  chfacfscmulgsum  23183  chfacfpmmul0  23185  chfacfpmmulgsum  23187  chfacfpmmulgsum2  23188  cayhamlem1  23189  cpmidgsumm2pm  23192  cpmidpmatlem2  23194  cpmadugsumlemB  23197  cpmadugsumlemC  23198  cpmadugsumlemF  23199  cpmadugsumfi  23200  cpmidgsum2  23202  cpmadumatpolylem2  23205  cayhamlem2  23207  chcoeffeqlem  23208  cayleyhamilton0  23212  cayleyhamiltonALT  23214  toponcom  23251  neitr  23503  cnprest  23612  nrmsep2  23679  bwth  23733  2ndcsep  23783  isref  23833  reghaus  24149  isfil2  24180  alexsubALTlem3  24373  cnextcn  24391  lpbl  24827  cmodscmulexp  25448  iscau4  25605  caussi  25623  cmetcusp  25680  ovolicc2lem3  25845  limcresi  26210  elply2  26519  elqaa  26650  aannenlem1  26660  aannenlem2  26661  relogbreexp  27108  cxplogb  27119  bpos1lem  27614  noetalem2  28104  tgjustc1  28942  tgjustc2  28943  axcont  29559  usgrexmplef  29845  subupgr  29873  cplgr3v  30021  cusgrfilem2  30042  usgredgsscusgredg  30045  rusgrprop0  30153  uspgr2wlkeqi  30233  trlontrl  30298  spthonpthon  30342  usgr2wlkspthlem1  30348  usgr2wlkspthlem2  30349  clwlkcompim  30372  clwlkl1loop  30375  wwlksnred  30486  clwwlknonwwlknonb  30702  clwwlknun  30708  1pthon2v  30759  frcond1  30872  frcond4  30876  frgrnbnb  30899  clwlknon2num  30974  numclwlk1lem1  30975  numclwlk1lem2  30976  numclwwlkovh  30979  numclwwlk2lem1  30982  numclwlk2lem2f  30983  numclwwlk2  30987  isgrpo  31104  vcz  31182  hvsub4  31644  hvaddsub4  31685  5oalem2  32262  5oalem5  32265  5oalem6  32266  3oalem2  32270  homcl  32353  hoadddi  32410  stle0i  32846  spansncv2  32900  mdsymlem1  33010  cdj3lem1  33041  f1ocnt  33438  gsumvsca1  33833  gsumvsca2  33834  crefdf  34526  sxbrsigalem0  34949  dya2icoseg2  34956  eulerpartlemgvv  35054  ballotlemirc  35210  bnj168  35407  bnj546  35572  bnj594  35588  bnj1097  35657  bnj1110  35658  bnj1174  35679  bnj1176  35681  axprALT2  35786  cusgredgex2  35983  acycgrislfgr  35993  umgracycusgr  35995  cusgracyclt3v  35997  satfv1  36214  satf0suclem  36226  fmlasuc0  36235  fmlafvel  36236  satffunlem2lem1  36255  satfun  36262  fv1stcnv  36633  colineardim1  36918  idinside  36941  finminlem  37198  ivthALT  37215  lukshef-ax2  37295  regsfromregtco  37418  bj-19.41al  37650  bj-equs45fv  37815  bj-elabd2ALT  37930  bj-rest10b  38102  copsex2b  38154  bj-elid6  38184  bj-ccinftydisj  38227  mptsnunlem  38354  topdifinffinlem  38363  relowlssretop  38379  elxp8  38387  fvineqsnf1  38426  pibt1  38432  poimirlem22  38653  poimirlem25  38656  poimirlem27  38658  poimirlem31  38662  ovoliunnfl  38673  itg2addnclem  38682  sstotbnd3  38803  heibor1lem  38836  heibor1  38837  rngmgmbs4  38958  exmid2  39124  redundss3  39737  redundpim3  39739  dalem53  40875  dalem54  40876  linepsubN  40902  pmapsub  40918  elpaddri  40952  pclfinN  41050  pclcmpatN  41051  cdlemg33c0  41852  dihatexv2  42489  eldioph4i  43912  acongtr  44078  pwfi2f1o  44191  aaitgo  44257  tfsconcat0b  44441  frege54cor0a  44956  clsf2  45219  ismnushort  45378  dvsconst  45407  mptssid  46346  xlimxrre  46934  icccncfext  46990  dvmptfprod  47048  stoweidlem17  47120  elaa2  47337  dmfcoafv  48338  elfzelfzlble  48484  prprelprb  48692  fmtnoprmfac1  48743  fmtnoprmfac2  48745  flsqrt  48771  lighneallem3  48785  proththd  48792  evenprm2  48905  gbogbow  48947  clnbgrel  49019  clnbgredg  49031  uhgrimisgrgric  49122  isubgr3stgrlem1  49157  isubgr3stgr  49166  gpg3nbgrvtx0  49267  gpgvtxdg3  49273  2zrngnmrid  49446  rhmsubcALTVlem3  49473  linccl  49619  lincvalpr  49623  lincdifsn  49629  lincext1  49659  lindslinindsimp1  49662  ldepspr  49678  lincresunit3lem1  49684  logblt1b  49769  dignnld  49808  dig1  49813  dignn0flhalflem1  49820  itcovalsucov  49873  line  49938  rrxline  49940  rrxsphere  49953  itschlc0xyqsol1  49971  itsclc0xyqsolr  49974  lubeldm2  50163  glbeldm2  50164  isinito4a  50779  alseuals  51088  ralseurals  51089  amgmwlem  51155