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 725  3anandis 918  sbimi 1171  equs45f 1198  eupickb 1433  2euex 1439  2exeu 1444  2eu1 1447  rcla42ev 1877  reu6 1928  pssn2lp 2143  difrab 2269  ssiun 2587  dfwe2 2930  trssord 2960  ordnbtwn 3058  tfi 3121  find 3150  imainss 3455  dffun7 3532  fof 3663  f1o2 3684  f1o3 3685  fv3 3724  fvelimab 3756  dff4 3807  dffo5 3812  f1ofv 3868  tfrlem5 3906  ssoprab2i 3999  ndmoprass 4040  ndmoprdistr 4041  omlimcl 4199  odi 4200  mapval2 4325  ixpf 4346  uniixp 4347  isfinite1 4516  infcntss 4536  isfinite 4614  nnsdom 4615  zfregs 4627  aceq6b 4722  ac6 4735  ac6s 4736  zorn 4777  ondomon 4836  cflim 4889  axregndlem1 4934  axregnd 4936  halfpq 5062  ltexprlem1 5122  ltexprlem4 5125  prlem936a 5133  reclem3pr 5138  recexsrlem 5192  suppsr3 5204  pre-axsup 5271  divcan5t 5745  divdivdivt 5749  divdivmult 5759  lediv2it 5853  nndivtrt 5915  lbreu 6000  supxr 6036  dfuz 6158  shftf 6296  fzrev2it 6453  seqzp1 6488  bcval2t 6905  clm4le 7027  climaddc1 7062  climsub 7074  climcmplem 7081  isummulc1ALT 7156  efsubt 7321  infxpidmlem11 7513  infxpidmlem12 7514  subtop 7596  islp2 7697  cnpco 7719  cncnp 7728  sncld 7737  blfval 7787  blssex 7806  iscms2 7944  bcthlem7 7955  isgrp 7991  vcz 8141  sspival 8344  ubthlem10 8482  spweu 8599  grothinf 8720  hvsub4t 8845  hvaddsub4t 8884  chsscm 9051  chcmh 9052  chocuni 9111  homclt 9464  osumlem5 9522  5oalem2 9540  5oalem5 9543  5oalem6 9544  3oalem2 9548  hoadddit 9669  lnopcon 9901  lnfncon 9928  stle0 10104  spansncv2t 10158  mdsymlem1 10267  cdj3lem1 10295  gelcomplOLD 10353  iintlem1 10512  trnij 10517

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