Theorem anim1i 334

Description: Introduce conjunct to both sides of an implication.

Hypothesis

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

Assertion

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

Proof of Theorem anim1i

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

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  pm5.61 447  sylanl1 460  sylanr1 462  3anandirs 921  sspr 2475  difex2 2877  mouniss 2890  cores 3499  fun11uni 3565  fabexg 3653  fores 3681  f1o2 3693  f1oabexg 3700  tz6.12-1 3736  ssimaex 3768  exfo 3822  tz7.48lem 3955  tz7.49c 3960  ndmoprass 4048  omass 4211  oewordri 4219  nnaordex 4249  nnawordex 4250  sbthlem9 4455  pssnn 4534  fiint 4559  fiintOLD 4560  abfii2OLD 4562  inf1 4607  infeq5 4621  rankuni 4698  ac6s2 4758  brdom5 4802  brdom4 4803  ltexpq 5080  prnmadd 5100  genpnnp 5108  prlem934 5139  prlem936 5155  reclem1pr 5156  reclem2pr 5157  suplem1pr 5161  suppsr2 5223  suppsr3 5224  cnegextlem3 5347  divasst 5741  lediv2it 5897  nn2get 5942  xrsupexmnf 6074  xrinfmexpnf 6075  xrsupsslem 6076  xrinfmsslem 6077  supxrre 6083  supxrun 6085  elnn0nn 6171  btwnz 6215  intfracqOLD 6255  qnegclt 6270  iooval2t 6367  ioo0t 6368  elioo4g 6385  elioc2t 6390  elico2t 6391  elicc2t 6392  elfzlem 6473  elfzp1 6510  expmwordit 6606  mulretOLD 6777  faclbnd 6945  faclbnd6 6954  bcval2t 6959  climshft2 7106  iserzshft2 7107  climmulc2 7129  climsubc2 7131  climcmplem 7137  isummulc1ALT 7213  rescncf 7272  abscncflem 7274  mulc1cncf 7279  dfef2 7307  reeff1olem1 7424  acdc5lem1 7491  infxpidmlem7 7558  infxpidmlem8 7559  infmap2lem1 7579  clscld 7683  islp2 7747  ismsg 7800  blssex 7854  opnin 7869  neibl 7877  lpbl 7880  lmbr 7928  metelcls 7965  metcnp4 7970  bcthlem2 8000  bcthlem14 8012  bcthlem15 8013  bcthlem30 8028  grpidinvlem3 8050  grpidinv 8052  ablmul 8131  isring 8141  nvlmle 8333  sspival 8397  nmobndseqi 8440  ubthlem3 8531  htthlem12 8631  efifolem4 8725  circgrp 8740  axhcompl 8868  hvaddsub4t 8945  hhcmpl 9069  hlimcaui 9106  ocsh 9156  chocuni 9172  projlem16 9201  5oalem2 9600  5oalem5 9603  3oalem2 9608  pjjs 9645  hoadddirt 9730  nmopub2tALT 9833  nmfnleub2t 9850  nmopcoadj 10034  leopmult 10067  stge1 10165  hatomistic 10289  mdsymlem2 10331  mdsymlem5 10334  infi 10578  infiOLD 10579  homib 10724

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