Theorem anim2i 362

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

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  sylanl2 510  sylanr2 512  anbi2i 538  biantrud 795  3anandis 1196  19.41 1448  sbimi 1537  equs45f 1569  eupickb 1836  2euexOLD 1845  2exeu 1850  2eu1 1853  r19.27av 2224  rcla42ev 2385  reu3 2444  pssn2lpOLD 2710  difrab 2868  ssiunOLD 3294  trssord 3675  ordnbtwn 3761  dfwe2OLD 3862  tfi 3937  find 3977  imainss 4331  dffun8OLD 4449  fof 4617  dff1o2OLD 4640  dff1o3OLD 4642  f1ocnv 4651  fv3 4690  fvelimab 4725  fvelimabOLD 4726  dff2 4789  dffo5 4794  dff1o6 4853  ssoprab2i 4937  ndmoprass 4981  ndmoprdistr 4982  tfrlem5 5123  omlimcl 5257  odi 5258  mapval2 5394  ixpf 5415  uniixp 5416  isfinite1 5624  infcntss 5646  isfinite 5741  nnsdom 5742  zfregs 5754  aceq6b 5904  ac6 5917  ac6s 5918  zorn 5959  ondomon 6008  cflim 6057  axregndlem1 6106  axregnd 6108  halfpq 6234  ltexprlem1 6294  ltexprlem4 6297  prlem936a 6305  reclem3pr 6310  recexsrlem 6364  suppsr3 6376  pre-axsup 6444  divadddiv 6960  lediv2a 7080  lbreu 7254  supxr 7290  dfuzi 7414  fzrev2i 7691  shftf 7764  seqzp1 7791  bcval2 8211  clm4lei 8341  climaddc1 8378  climsub 8390  climcmplem 8397  isummulc1iALT 8474  infxpidmlem11 8831  infxpidmlem12 8832  subtop 8916  islp2 9023  cnpco 9046  cncnp 9055  sncld 9064  blfval 9112  blssex 9131  iscms2 9272  bcthlem7 9283  isgrp 9321  gxsub 9399  isga2 9452  gapmlem 9461  vcz 9521  sspival 9736  ubthlem10 9881  spweu 10000  grothpw 10134  grothpwex 10135  grothomex 10136  indexfi 10174  isflimf 10323  rngmgmbs4 10401  hvsub4 10538  hvaddsub4 10578  chsscmi 10745  chcmhi 10746  chocunii 10805  homcl 11157  osumlem5 11217  5oalem2 11235  5oalem5 11238  5oalem6 11239  3oalem2 11243  hoadddi 11366  lnopconi 11600  lnfnconi 11627  stle0i 11811  spansncv2 11865  mdsymlem1 11975  cdj3lem1 12006  bnj44OLD 12420  bnj143 12475  bnj168 12496  bnj512 12519  bnj1064 12900  bnj1167 12959  bnj518 13260  bnj546 13272  bnj583 13296  bnj594 13300  bnj1097 13412  bnj1100 13414  bnj1174 13442  dvdsnegb 13672  ndvdssub 13710  ordsucuniel 13863  lukshef-ax2 14239  dff1o6f 14416  isfinite1b 14434  sallnei 14873  cntrsetlem 14999  iintlem1 15010  trnij 15015  cptarc 15242  finminlem 15367  alexsublem3 15439  reconn 15451  ivthALT 15454  topfneec 15501  neibastop2lem3 15521  limfilcf 15587  flimfcls 15613  difxp 15690  indexa 15753  indexfiOLD 15755  frminex 15773  elfzp12 15795  totbndbnd 15944  rrntotbnd 16022  phtpycolem3 16053  phtpycolem4 16054  pcoloopf 16079  strss 16711  linepsub 17232  pmapsub 17250  elpaddri 17263

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 164  df-an 242

Copyright terms: Public domain