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

Theorem imim2i 13
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 10 . 2  |-  ( ch 
->  ( ph  ->  ps ) )
32a2i 12 1  |-  ( ( ch  ->  ph )  -> 
( ch  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  imim12i  53  imim3i  55  ja  153  imim21b  356  pm3.48  806  jcab  833  exbir  1355  nic-ax  1428  nic-axALT  1429  tbw-bijust  1453  merco1  1468  sbimi  1633  19.24  1673  19.21h  1731  nfimd  1761  19.21t  1790  ax12olem3  1870  ax11indi  2135  mopick  2205  r19.36av  2688  ceqsalt  2810  vtoclgft  2834  spcgft  2860  mo2icl  2944  euind  2952  reu6  2954  reuind  2968  sbciegft  3021  dfiin2g  3936  invdisj  4012  elpwunsn  4568  tfindsg  4651  findsg  4683  dff3  5673  zfrep6  5748  fnoprabg  5945  tz7.48-1  6455  odi  6577  r1sdom  7446  kmlem6  7781  kmlem12  7787  zorng  8131  squeeze0  9659  xrsupexmnf  10623  xrinfmexpnf  10624  rexanre  11830  tgcnp  16983  lmcvg  16992  iblcnlem  19143  limcresi  19235  isch3  21821  disjexc  23177  cntmeas  23553  axextdfeq  24154  hbimtg  24163  meran3  24852  waj-ax  24853  lukshef-ax2  24854  imsym1  24857  wl-adnestantALT  24907  domrngref  25060  qusp  25542  bwt2  25592  nn0prpw  26239  ismrc  26776  pm11.71  27596  atbiffatnnbalt  27883  cusgrauvtx  28168  a9e2ndeqVD  28685  a9e2ndeqALT  28708  bnj900  28961  bnj1172  29031  bnj1174  29033  bnj1176  29035  ltrnnid  30325
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator