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

Theorem anim2i 334
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 331 1  |-  ( ( ch  /\  ph )  ->  ( ch  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  sylanl2  395  sylanr2  397  andi  767  pm4.55dc  884  xoranor  1313  19.41h  1620  sbimi  1694  equs5e  1723  exdistrfor  1728  equs45f  1730  sbidm  1779  eu3h  1993  eupickb  2029  2exeu  2040  darii  2048  festino  2054  baroco  2055  r19.27av  2504  rspc2ev  2735  reu3  2803  difdif  3123  ssddif  3231  inssdif  3233  difin  3234  difindiss  3251  indifdir  3253  difrab  3271  iundif2ss  3790  trssord  4198  ordsuc  4369  find  4404  imainss  4834  dffun5r  5014  fof  5217  f1ocnv  5250  fv3  5312  relelfvdm  5320  funimass4  5339  fvelimab  5344  funconstss  5401  dff2  5427  dffo5  5432  dff1o6  5537  oprabid  5663  ssoprab2i  5719  releldm2  5937  recexgt0sr  7298  lediv2a  8328  lbreu  8378  elfzp12  9480  focdmex  10160  fihashf1rn  10162  cau3lem  10512  fsumcl2lem  10755  dvdsnegb  10906  dvds2add  10923  dvds2sub  10924  ndvdssub  11023  gcd2n0cl  11054  divgcdcoprmex  11177  cncongr1  11178
  Copyright terms: Public domain W3C validator