Theorem anim2i 342

Description: Introduce conjunct to both sides of an implication.

Hypothesis

Ref	Expression
anim1i.1	|- (ph -> ps)

Assertion

Ref	Expression
anim2i	|- ((ch /\ ph) -> (ch /\ ps))

Proof of Theorem anim2i

Step	Hyp	Ref	Expression
1		id 59	. 2 |- (ch -> ch)
2		anim1i.1	. 2 |- (ph -> ps)
3	1, 2	anim12i 340	1 |- ((ch /\ ph) -> (ch /\ ps))

Syntax hints:   -> wi 3   /\ wa 230

This theorem is referenced by:  sylanl2 472  sylanr2 474  anbi2i 491  biantrud 738  3anandis 932  sbimi 1215  equs45f 1242  eupickb 1478  2euex 1484  2exeu 1489  2eu1 1492  rcla42ev 1928  reu6 1979  pssn2lp 2198  difrab 2324  ssiun 2646  dfwe2 2992  trssord 3022  ordnbtwn 3120  tfi 3183  find 3212  imainss 3520  dffun7 3597  fof 3729  f1o2 3750  f1o3 3751  fv3 3790  fvelimab 3822  dff4 3873  dffo5 3878  f1ofv 3935  tfrlem5 3973  ssoprab2i 4066  ndmoprass 4106  ndmoprdistr 4107  omlimcl 4267  odi 4268  mapval2 4396  ixpf 4417  uniixp 4418  isfinite1 4595  infcntss 4616  isfinite 4696  nnsdom 4697  zfregs 4709  aceq6b 4804  ac6 4817  ac6s 4818  zorn 4859  ondomon 4921  cflim 4974  axregndlem1 5019  axregnd 5021  halfpq 5147  ltexprlem1 5207  ltexprlem4 5210  prlem936a 5218  reclem3pr 5223  recexsrlem 5277  suppsr3 5289  pre-axsup 5356  divcan5 5839  divdivdiv 5843  divdivmul 5853  lediv2a 5957  nndivtr 6021  lbreu 6127  supxr 6163  dfuzi 6287  fzrev2i 6539  shftf 6610  seqzp1 6637  bcval2 7049  clm4lei 7171  climaddc1 7208  climsub 7220  climcmplem 7227  isummulc1iALT 7303  efsub 7461  infxpidmlem11 7654  infxpidmlem12 7655  subtop 7733  islp2 7832  cnpco 7854  cncnp 7863  sncld 7872  blfval 7920  blssex 7939  iscms2 8079  bcthlem7 8090  isgrp 8126  vcz 8273  sspival 8481  ubthlem10 8622  spweu 8741  grothinf 8864  hvsub4 8989  hvaddsub4 9028  chsscmi 9195  chcmhi 9196  chocunii 9255  homcl 9607  osumlem5 9665  5oalem2 9683  5oalem5 9686  5oalem6 9687  3oalem2 9691  hoadddi 9812  lnopconi 10046  lnfnconi 10073  stle0i 10250  spansncv2 10304  mdsymlem1 10414  cdj3lem1 10445  iintlem1 10714  trnij 10719

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 154  df-an 232

Copyright terms: Public domain