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 918  sspr 2466  difex2 2867  mouniss 2880  cores 3485  fun11uni 3551  fabexg 3638  fores 3666  f1o2 3678  f1oabexg 3685  tz6.12-1 3721  ssimaex 3753  exfo 3807  tz7.48lem 3940  tz7.49c 3945  ndmoprass 4034  omass 4195  oewordri 4203  nnaordex 4233  nnawordex 4234  sbthlem9 4435  pssnn 4513  fiint 4534  abfii2 4536  inf1 4579  infeq5 4593  rankuni 4670  ac6s2 4730  brdom5 4774  brdom4 4775  ltexpq 5052  prnmadd 5072  genpnnp 5080  prlem934 5111  prlem936 5127  reclem1pr 5128  reclem2pr 5129  suplem1pr 5133  suppsr2 5195  suppsr3 5196  cnegextlem3 5319  divasst 5704  lediv2it 5845  nn2get 5890  xrsupexmnf 6021  xrinfmexpnf 6022  xrsupsslem 6023  xrinfmsslem 6024  supxrre 6030  supxrun 6032  elnn0nn 6118  btwnz 6163  qnegclt 6208  iooval2t 6304  ioo0t 6305  elioo4g 6318  elioc2t 6322  elico2t 6323  elicc2t 6324  elfzlem 6405  elfzp1 6442  expmwordit 6537  faclbnd 6882  faclbnd6 6891  bcval2t 6897  climshft2 7043  iserzshft2 7044  climmulc2 7065  climsubc2 7067  climcmplem 7073  isummulc1ALT 7148  rescncf 7207  abscncflem 7209  mulc1cncf 7214  dfef2 7249  reeff1olem1 7364  reeff1olem1OLD 7366  acdc5lem1 7433  infxpidmlem7 7501  infxpidmlem8 7502  infmap2lem1 7521  clscld 7625  islp2 7688  ismsg 7739  blssex 7794  opnin 7809  neibl 7817  lpbl 7819  lmbr 7866  metelcls 7900  metcnp4 7904  bcthlem2 7934  bcthlem14 7946  bcthlem15 7947  bcthlem30 7962  grpidinvlem3 7984  grpidinv 7986  ablmul 8068  isring 8078  isvcgOLD 8133  nvlmle 8268  sspival 8331  nmobndseqi 8372  ubthlem3 8462  htthlem12 8561  efifolem4 8640  circgrp 8660  hvaddsub4t 8866  hhcmpl 8990  hlimcaui 9027  ocsh 9072  chocuni 9088  projlem16 9117  5oalem2 9517  5oalem5 9520  3oalem2 9525  pjjs 9562  hoadddirt 9647  nmopub2tALT 9750  nmfnleub2t 9766  nmopcoadj 9948  leopmult 9979  stge1 10075  hatomistic 10197  mdsymlem2 10239  mdsymlem5 10242  infi 10448  homib 10568

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