HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
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
StepHypRef Expression
1 id 59 . 2 |- (ch -> ch)
2 anim1i.1 . 2 |- (ph -> ps)
31, 2anim12i 333 1 |- ((ch /\ ph) -> (ch /\ ps))
Colors of variables: wff set class
Syntax hints:   -> wi 3   /\ wa 223
This theorem is referenced by:  sylanl2 461  sylanr2 463  anbi2i 479  biantrud 724  3anandis 917  sbimi 1169  equs45f 1196  eupickb 1428  2euex 1434  2exeu 1439  2eu1 1442  rcla42ev 1872  reu6 1922  pssn2lp 2137  difrab 2263  ssiun 2582  dfwe2 2925  trssord 2955  ordnbtwn 3053  tfi 3116  find 3145  imainss 3449  dffun7 3526  fof 3657  f1o2 3678  f1o3 3679  fv3 3718  fvelimab 3750  dff4 3801  dffo5 3806  f1ofv 3862  tfrlem5 3900  ssoprab2i 3993  ndmoprass 4034  ndmoprdistr 4035  omlimcl 4193  odi 4194  mapval2 4319  ixpf 4340  uniixp 4341  isfinite1 4510  infcntss 4530  isfinite 4606  nnsdom 4607  zfregs 4619  aceq6b 4714  ac6 4727  ac6s 4728  zorn 4769  ondomon 4828  cflim 4881  axregndlem1 4926  axregnd 4928  halfpq 5054  ltexprlem1 5114  ltexprlem4 5117  prlem936a 5125  reclem3pr 5130  recexsrlem 5184  suppsr3 5196  pre-axsup 5263  divcan5t 5737  divdivdivt 5741  divdivmult 5751  lediv2it 5845  nndivtrt 5907  lbreu 5992  supxr 6028  dfuz 6150  shftf 6288  fzrev2it 6445  seqzp1 6480  bcval2t 6897  clm4le 7019  climaddc1 7054  climsub 7066  climcmplem 7073  isummulc1ALT 7148  efsubt 7313  infxpidmlem11 7505  infxpidmlem12 7506  subtop 7588  islp2 7688  cnpco 7708  cncnp 7717  sncld 7726  blfval 7775  blssex 7794  iscms2 7928  bcthlem7 7939  isgrp 7975  vcz 8126  sspival 8331  ubthlem10 8469  spweu 8581  grothinf 8720  hvsub4t 8827  hvaddsub4t 8866  chsscm 9033  chcmh 9034  chocuni 9088  homclt 9441  osumlem5 9499  5oalem2 9517  5oalem5 9520  5oalem6 9521  3oalem2 9525  hoadddit 9646  lnopcon 9878  lnfncon 9905  stle0 10076  spansncv2t 10130  mdsymlem1 10238  cdj3lem1 10266  iintlem1 10476  trnij 10481
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