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-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  imim12i  57  imim3i  59  imim21b  245  jcab  545  pm3.48  709  con1dc  764  jadc  771  pm4.78i  819  pm5.6r  847  exbir  1341  19.21h  1465  nford  1475  19.21ht  1489  exim  1506  i19.24  1546  equsexd  1633  equvini  1657  nfexd  1660  sbimi  1663  sbcof2  1707  nfsb2or  1734  mopick  1994  r19.32r  2474  r19.36av  2478  ceqsalt  2597  vtoclgft  2621  spcgft  2647  spcegft  2649  elab3gf  2714  mo2icl  2742  euind  2750  reu6  2752  reuind  2766  sbciegft  2815  ssddif  3198  dfiin2g  3717  invdisj  3786  ordunisuc2r  4267  fnoprabg  5629  caucvgsr  6943  elabgft1  10283  bj-nntrans  10442
  Copyright terms: Public domain W3C validator