ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  anim2i Unicode version

Theorem anim2i 339
Description: Introduce conjunct to both sides of an implication. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
anim1i.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
anim2i  |-  ( ( ch  /\  ph )  ->  ( ch  /\  ps ) )

Proof of Theorem anim2i
StepHypRef Expression
1 id 19 . 2  |-  ( ch 
->  ch )
2 anim1i.1 . 2  |-  ( ph  ->  ps )
31, 2anim12i 336 1  |-  ( ( ch  /\  ph )  ->  ( ch  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  sylanl2  400  sylanr2  402  andi  792  pm4.55dc  907  xoranor  1340  19.41h  1648  sbimi  1722  equs5e  1751  exdistrfor  1756  equs45f  1758  sbidm  1807  eu3h  2022  eupickb  2058  2exeu  2069  darii  2077  festino  2083  baroco  2084  r19.27v  2536  r19.27av  2544  rspc2ev  2778  reu3  2847  difdif  3171  ssddif  3280  inssdif  3282  difin  3283  difindiss  3300  indifdir  3302  difrab  3320  iundif2ss  3848  trssord  4272  ordsuc  4448  find  4483  imainss  4924  dffun5r  5105  fof  5315  f1ocnv  5348  fv3  5412  relelfvdm  5421  funimass4  5440  fvelimab  5445  funconstss  5506  dff2  5532  dffo5  5537  dff1o6  5645  oprabid  5771  ssoprab2i  5828  releldm2  6051  ixpf  6582  recexgt0sr  7549  map2psrprg  7581  lediv2a  8617  lbreu  8667  elfzp12  9834  focdmex  10488  fihashf1rn  10490  cau3lem  10841  fsumcl2lem  11122  dvdsnegb  11422  dvds2add  11439  dvds2sub  11440  ndvdssub  11539  gcd2n0cl  11570  divgcdcoprmex  11695  cncongr1  11696  ctinfom  11852  istopfin  12078  toponcom  12105  cnptoprest  12319
  Copyright terms: Public domain W3C validator