Theorem anim2i 270

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 9	. 2 |- (ch -> ch)
2		anim1i.1	. 2 |- (ph -> ps)
3	1, 2	anim12i 268	1 |- ((ch /\ ph) -> (ch /\ ps))

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  sylan12 355  anbi2i 367  biantrud 545  sbimi 854  eupickb 1056  2euex 1061  2exeu 1066  2eu1 1067  rcla42ev 1405  pssn2lp 1571  difrab 1695  ssiun 2018  dfwe2 2187  trssord 2216  tfi 2244  ordnbtwn 2316  find 2396  imainss 2649  dffun7 2688  fof 2788  f1o2 2804  f1o3 2805  fv3 2839  tfrlem5 2953  tfrlem8 2956  ssoprab2i 3036  ndmoprass 3062  ndmoprdistr 3063  isfinite1 3425  infcntss 3443  isfinite 3480  nnsdom 3481  zfregs 3491  aceq6b 3565  ac6 3576  ac6s 3577  zorn2 3612  ondomon 3662  cflim 3704  axregndlem1 3748  axregnd 3750  halfpq 3876  ltexprlem1 3936  ltexprlem4 3939  prlem936a 3947  reclem3pr 3952  recexsrlem 4006  suppsr3 4018  axsup 4088  divdivdivt 4265  infxpidmlem11 4943  infxpidmlem12 4944  hvsub4t 5014  chsscm 5147  chcmh 5148  chocuni 5179  osumlem5 5534  5oalem2 5545  5oalem5 5548  5oalem6 5549  3oalem2 5553  stle0 5680  spansncv2t 5725

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org