Theorem anim2i 616

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  sylanr2  682  andi  1008  19.41v  1949  exdistrf  2455  equs45f  2467  moaneu  2626  dariiALT  2669  festinoALT  2678  barocoALT  2680  r19.27v  3194  rspc2ev  3648  reu3  3749  difrab  4337  opthprneg  4889  copsexgw  5510  copsexg  5511  imainss  6185  trssord  6412  ordnbtwn  6488  fof  6834  fv3  6938  fvelimab  6994  dff2  7133  dffo5  7138  foco2  7143  fnsnb  7200  tpres  7238  f13dfv  7310  dff1o6  7311  oprabidw  7479  oprabid  7480  ssoprab2i  7561  ndmovass  7638  ndmovdistr  7639  elovmpt3rab1  7710  tfi  7890  find  7935  releldm2  8084  bropopvvv  8131  bropfvvvvlem  8132  ressuppssdif  8226  omlimcl  8634  odi  8635  ixpf  8978  dif1en  9226  domtrfil  9258  funsnfsupp  9461  hartogs  9613  card2on  9623  zfreg  9664  epfrs  9800  acni3  10116  dfac2b  10200  cflm  10319  axdc2lem  10517  ac6s  10553  ondomon  10632  axregndlem1  10671  axregnd  10673  eltsk2g  10820  grothpw  10895  grothpwex  10896  grothomex  10898  ltexprlem1  11105  ltexprlem4  11108  recexsrlem  11172  elfzp12  13663  hashf1rn  14401  hashdifpr  14464  hashgt23el  14473  hashge2el2dif  14529  ccatsymb  14630  swrdnd0  14705  swrdpfx  14755  pfxpfx  14756  pfxccatin12  14781  cshwidxmod  14851  repswcshw  14860  cshimadifsn  14878  cshimadifsn0  14879  pfxco  14887  wwlktovfo  15007  relexpsucnnl  15079  cau3lem  15403  rlimres  15604  dvdsnegb  16322  dvds2add  16338  dvds2sub  16339  nn0onn  16428  gcd2n0cl  16555  lcmfun  16692  divgcdcoprmex  16713  cncongr1  16714  isfunc  17928  drsdirfi  18375  sgrpidmnd  18777  smndex1iidm  18936  gaid  19339  symg2bas  19434  qusecsub  19877  c0mgm  20485  rhmisrnghm  20506  c0rhm  20560  rhmsubcrngclem1  20688  srhmsubclem1  20699  abvn0b  20859  lmhmlem  21051  prmirredlem  21506  psgndiflemB  21641  matsubgcell  22461  tposmap  22484  mat1dim0  22500  mat1dimid  22501  mat1dimscm  22502  mat1dimmul  22503  dmatmul  22524  dmatcrng  22529  scmatcrng  22548  scmatf1  22558  1marepvsma1  22610  maducoeval2  22667  smadiadetlem3lem0  22692  slesolinv  22707  cramerimplem1  22710  cramerimplem2  22711  1pmatscmul  22729  cpmatacl  22743  cpmatmcllem  22745  cpmatmcl  22746  mat2pmatf1  22756  mat2pmatghm  22757  mat2pmatmul  22758  mat2pmatlin  22762  mat2pmatscmxcl  22767  m2cpmmhm  22772  m2pmfzgsumcl  22775  decpmatmul  22799  pmatcollpw2lem  22804  monmatcollpw  22806  pmatcollpwfi  22809  pmatcollpw3fi1lem2  22814  pmatcollpwscmatlem1  22816  pmatcollpwscmatlem2  22817  pmatcollpwscmat  22818  pm2mpghm  22843  pm2mpmhmlem2  22846  pm2mp  22852  chmatcl  22855  chmatval  22856  chmaidscmat  22875  chfacfisf  22881  chfacfisfcpmat  22882  chfacfscmulcl  22884  chfacfscmul0  22885  chfacfscmulgsum  22887  chfacfpmmul0  22889  chfacfpmmulgsum  22891  chfacfpmmulgsum2  22892  cayhamlem1  22893  cpmidgsumm2pm  22896  cpmidpmatlem2  22898  cpmadugsumlemB  22901  cpmadugsumlemC  22902  cpmadugsumlemF  22903  cpmadugsumfi  22904  cpmidgsum2  22906  cpmadumatpolylem2  22909  cayhamlem2  22911  chcoeffeqlem  22912  cayleyhamilton0  22916  cayleyhamiltonALT  22918  toponcom  22955  neitr  23209  cnprest  23318  nrmsep2  23385  bwth  23439  2ndcsep  23488  isref  23538  reghaus  23854  isfil2  23885  alexsubALTlem3  24078  cnextcn  24096  lpbl  24537  cmodscmulexp  25174  iscau4  25332  caussi  25350  cmetcusp  25407  ovolicc2lem3  25573  limcresi  25940  elply2  26255  elqaa  26382  aannenlem1  26388  aannenlem2  26389  relogbreexp  26836  cxplogb  26847  bpos1lem  27344  noetalem2  27805  tgjustc1  28501  tgjustc2  28502  axcont  29009  usgrexmplef  29294  subupgr  29322  cplgr3v  29470  cusgrfilem2  29492  usgredgsscusgredg  29495  rusgrprop0  29603  uspgr2wlkeqi  29684  trlontrl  29747  spthonpthon  29787  usgr2wlkspthlem1  29793  usgr2wlkspthlem2  29794  clwlkcompim  29816  clwlkl1loop  29819  wwlksnred  29925  clwwlknonwwlknonb  30138  clwwlknun  30144  1pthon2v  30185  frcond1  30298  frcond4  30302  frgrnbnb  30325  clwlknon2num  30400  numclwlk1lem1  30401  numclwlk1lem2  30402  numclwwlkovh  30405  numclwwlk2lem1  30408  numclwlk2lem2f  30409  numclwwlk2  30413  isgrpo  30529  vcz  30607  hvsub4  31069  hvaddsub4  31110  5oalem2  31687  5oalem5  31690  5oalem6  31691  3oalem2  31695  homcl  31778  hoadddi  31835  stle0i  32271  spansncv2  32325  mdsymlem1  32435  cdj3lem1  32466  f1ocnt  32807  gsumle  33074  gsumvsca1  33205  gsumvsca2  33206  crefdf  33794  sxbrsigalem0  34236  dya2icoseg2  34243  eulerpartlemgvv  34341  ballotlemirc  34496  bnj168  34706  bnj546  34872  bnj594  34888  bnj1097  34957  bnj1110  34958  bnj1174  34979  bnj1176  34981  cusgredgex2  35090  acycgrislfgr  35120  umgracycusgr  35122  cusgracyclt3v  35124  satfv1  35331  satf0suclem  35343  fmlasuc0  35352  fmlafvel  35353  satffunlem2lem1  35372  satfun  35379  fv1stcnv  35740  colineardim1  36025  idinside  36048  finminlem  36284  ivthALT  36301  lukshef-ax2  36381  bj-19.41al  36625  bj-equs45fv  36777  bj-elabd2ALT  36891  bj-rest10b  37055  copsex2b  37106  bj-elid6  37136  bj-ccinftydisj  37179  mptsnunlem  37304  topdifinffinlem  37313  relowlssretop  37329  elxp8  37337  fvineqsnf1  37376  pibt1  37382  matunitlindflem1  37576  poimirlem22  37602  poimirlem25  37605  poimirlem27  37607  poimirlem31  37611  ovoliunnfl  37622  itg2addnclem  37631  sstotbnd3  37736  heibor1lem  37769  heibor1  37770  rngmgmbs4  37891  exmid2  38059  redundss3  38584  redundpim3  38586  dalem53  39682  dalem54  39683  linepsubN  39709  pmapsub  39725  elpaddri  39759  pclfinN  39857  pclcmpatN  39858  cdlemg33c0  40659  dihatexv2  41296  eldioph4i  42768  acongtr  42935  pwfi2f1o  43053  aaitgo  43119  tfsconcat0b  43308  frege54cor0a  43825  clsf2  44088  ismnushort  44270  dvsconst  44299  mptssid  45149  xlimxrre  45752  icccncfext  45808  stoweidlem17  45938  elaa2  46155  dmfcoafv  47090  elfzelfzlble  47236  prprelprb  47391  fmtnoprmfac1  47439  fmtnoprmfac2  47441  flsqrt  47467  lighneallem3  47481  proththd  47488  evenprm2  47588  gbogbow  47630  clnbgrel  47701  clnbgredg  47712  uhgrimisgrgric  47783  2zrngnmrid  47979  rhmsubcALTVlem3  48006  linccl  48143  lincvalpr  48147  lincdifsn  48153  lincext1  48183  lindslinindsimp1  48186  ldepspr  48202  lincresunit3lem1  48208  logblt1b  48298  dignnld  48337  dig1  48342  dignn0flhalflem1  48349  itcovalsucov  48402  line  48466  rrxline  48468  rrxsphere  48482  itschlc0xyqsol1  48500  itsclc0xyqsolr  48503  lubeldm2  48636  glbeldm2  48637  amgmwlem  48896