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

Theorem imim2i 12
Description: Inference adding common antecedents in an implication. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
imim2i.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
imim2i  |-  ( ( ch  ->  ph )  -> 
( ch  ->  ps ) )

Proof of Theorem imim2i
StepHypRef Expression
1 imim2i.1 . . 3  |-  ( ph  ->  ps )
21a1i 9 . 2  |-  ( ch 
->  ( ph  ->  ps ) )
32a2i 11 1  |-  ( ( ch  ->  ph )  -> 
( ch  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  imim12i  59  imim3i  61  imim21b  251  jcab  598  pm4.78i  777  pm3.48  780  con1dc  851  jadc  858  pm5.6r  922  exbir  1429  19.21h  1550  nford  1560  19.21ht  1574  exim  1592  i19.24  1632  equsexd  1722  equvini  1751  nfexd  1754  sbimi  1757  sbcof2  1803  nfsb2or  1830  mopick  2097  r19.32r  2616  r19.36av  2621  ceqsalt  2756  vtoclgft  2780  spcgft  2807  spcegft  2809  elab3gf  2880  mo2icl  2909  euind  2917  reu6  2919  reuind  2935  sbciegft  2985  ssddif  3361  dfiin2g  3904  invdisj  3981  ordunisuc2r  4496  fnoprabg  5952  caucvgsr  7757  rexanre  11177  tgcnp  12968  lmcvg  12976  elabgft1  13778  bj-nntrans  13951
  Copyright terms: Public domain W3C validator