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

Theorem imim2i 14
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 11 . 2  |-  ( ch 
->  ( ph  ->  ps ) )
32a2i 13 1  |-  ( ( ch  ->  ph )  -> 
( ch  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  imim12i  55  imim3i  57  ja  155  imim21b  357  pm3.48  807  jcab  834  exbir  1374  nic-ax  1447  nic-axALT  1448  tbw-bijust  1472  merco1  1487  sbimi  1664  19.24  1674  nfimdOLD  1828  19.21hOLD  1862  19.21tOLD  1886  ax12olem3OLD  2013  ax11indi  2272  mopick  2342  axi5r  2408  r19.36av  2848  ceqsalt  2970  vtoclgft  2994  spcgft  3020  mo2icl  3105  euind  3113  reu6  3115  reuind  3129  sbciegft  3183  dfiin2g  4116  invdisj  4193  elpwunsn  4749  tfindsg  4832  findsg  4864  dff3  5874  zfrep6  5960  fnoprabg  6163  tz7.48-1  6692  odi  6814  r1sdom  7692  kmlem6  8027  kmlem12  8033  zorng  8376  squeeze0  9905  xrsupexmnf  10875  xrinfmexpnf  10876  rexanre  12142  tgcnp  17309  lmcvg  17318  bwth  17465  iblcnlem  19672  limcresi  19764  isch3  22736  disjexc  24025  cntmeas  24572  axextdfeq  25417  hbimtg  25426  meran3  26155  waj-ax  26156  lukshef-ax2  26157  imsym1  26160  wl-adnestantALT  26210  nn0prpw  26317  ismrc  26746  pm11.71  27564  a9e2ndeqVD  28958  a9e2ndeqALT  28980  bnj900  29237  bnj1172  29307  bnj1174  29309  bnj1176  29311  ax12olem3aAUX7  29394  ltrnnid  30870
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator