Theorem anim2i 335

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 333	1 |- ((ch /\ ph) -> (ch /\ ps))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  sylanl2 461  sylanr2 463  anbi2i 480  biantrud 726  3anandis 920  sbimi 1173  equs45f 1200  eupickb 1435  2euex 1441  2exeu 1446  2eu1 1449  rcla42ev 1881  reu6 1932  pssn2lp 2147  difrab 2273  ssiun 2592  dfwe2 2935  trssord 2965  ordnbtwn 3063  tfi 3126  find 3155  imainss 3463  dffun7 3540  fof 3672  f1o2 3693  f1o3 3694  fv3 3733  fvelimab 3765  dff4 3816  dffo5 3821  f1ofv 3877  tfrlem5 3915  ssoprab2i 4008  ndmoprass 4048  ndmoprdistr 4049  omlimcl 4209  odi 4210  mapval2 4335  ixpf 4356  uniixp 4357  isfinite1OLD 4531  infcntss 4554  isfiniteOLD 4634  nnsdom 4635  zfregs 4647  aceq6b 4742  ac6 4755  ac6s 4756  zorn 4797  ondomon 4856  cflim 4909  axregndlem1 4954  axregnd 4956  halfpq 5082  ltexprlem1 5142  ltexprlem4 5145  prlem936a 5153  reclem3pr 5158  recexsrlem 5212  suppsr3 5224  pre-axsup 5291  divcan5t 5781  divdivdivt 5785  divdivmult 5795  lediv2it 5897  nndivtrt 5960  lbreu 6045  supxr 6081  dfuz 6202  intfracqOLD 6255  shftf 6351  fzrev2it 6513  seqzp1 6548  bcval2t 6959  clm4le 7081  climaddc1 7118  climsub 7130  climcmplem 7137  isummulc1ALT 7213  efsubt 7371  infxpidmlem11 7562  infxpidmlem12 7563  subtop 7646  islp2 7747  cnpco 7769  cncnp 7778  sncld 7787  blfval 7835  blssex 7854  iscms2 7994  bcthlem7 8005  isgrp 8041  vcz 8189  sspival 8397  ubthlem10 8538  spweu 8657  grothinf 8781  hvsub4t 8906  hvaddsub4t 8945  chsscm 9112  chcmh 9113  chocuni 9172  homclt 9524  osumlem5 9582  5oalem2 9600  5oalem5 9603  5oalem6 9604  3oalem2 9608  hoadddit 9729  lnopcon 9963  lnfncon 9990  stle0 10166  spansncv2t 10220  mdsymlem1 10330  cdj3lem1 10361  iintlem1 10632  trnij 10637

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 147  df-an 225

Copyright terms: Public domain