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  592  pm4.78i  771  pm3.48  774  con1dc  841  jadc  848  pm5.6r  912  exbir  1412  19.21h  1536  nford  1546  19.21ht  1560  exim  1578  i19.24  1618  equsexd  1707  equvini  1731  nfexd  1734  sbimi  1737  sbcof2  1782  nfsb2or  1809  mopick  2077  r19.32r  2578  r19.36av  2582  ceqsalt  2712  vtoclgft  2736  spcgft  2763  spcegft  2765  elab3gf  2834  mo2icl  2863  euind  2871  reu6  2873  reuind  2889  sbciegft  2939  ssddif  3310  dfiin2g  3846  invdisj  3923  ordunisuc2r  4430  fnoprabg  5872  caucvgsr  7617  rexanre  10999  tgcnp  12388  lmcvg  12396  elabgft1  13015  bj-nntrans  13179
  Copyright terms: Public domain W3C validator