MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imim2i Structured version   Unicode version

Theorem imim2i 16
Description: Inference adding common antecedents in an implication. Inference associated with imim2 55. Its associated inference is syl 17. (Contributed by NM, 28-Dec-1992.)
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 11 . 2  |-  ( ch 
->  ( ph  ->  ps ) )
32a2i 14 1  |-  ( ( ch  ->  ph )  -> 
( ch  ->  ps ) )
Colors of variables: wff setvar 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  imim12  100  ja  164  imim21b  368  pm3.48  841  jcab  871  nic-ax  1552  nic-axALT  1553  tbw-bijust  1577  merco1  1592  sbimi  1792  19.24  1805  19.23v  1807  2eu6  2356  axi5r  2392  r19.36v  2976  ceqsalt  3104  vtoclgft  3129  spcgft  3158  mo2icl  3250  euind  3258  reu6  3260  reuind  3275  sbciegft  3330  elpwunsn  4037  dfiin2g  4329  invdisj  4409  dff3  6046  fnoprabg  6407  tfindsg  6697  findsg  6730  zfrep6  6771  tz7.48-1  7164  odi  7284  r1sdom  8246  kmlem6  8585  kmlem12  8591  zorng  8934  squeeze0  10509  xrsupexmnf  11590  xrinfmexpnf  11591  mptnn0fsuppd  12209  reuccats1lem  12826  rexanre  13397  pmatcollpw2lem  19787  tgcnp  20255  lmcvg  20264  iblcnlem  22732  limcresi  22826  isch3  26879  disjexc  28192  cntmeas  29043  bnj900  29735  bnj1172  29805  bnj1174  29807  bnj1176  29809  axextdfeq  30438  hbimtg  30447  nn0prpw  30971  meran3  31065  waj-ax  31066  lukshef-ax2  31067  imsym1  31070  bj-andnotim  31163  bj-19.21bit  31230  bj-ceqsalt0  31439  bj-ceqsalt1  31440  wl-embantALT  31760  contrd  32246  ax12indi  32433  ltrnnid  33619  ismrc  35461  rp-fakenanass  36078  frege55lem1a  36319  frege55lem1b  36348  frege55lem1c  36369  frege92  36408  pm11.71  36604  exbir  36690  ax6e2ndeqVD  37166  ax6e2ndeqALT  37188  nn0sumshdiglemA  39703  nn0sumshdiglemB  39704
  Copyright terms: Public domain W3C validator