MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imim2i 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  1371  nic-ax  1444  nic-axALT  1445  tbw-bijust  1469  merco1  1484  sbimi  1659  19.24  1669  nfimdOLD  1818  19.21hOLD  1852  19.21tOLD  1875  ax12olem3OLD  1967  ax11indi  2230  mopick  2300  axi5r  2360  r19.36av  2799  ceqsalt  2921  vtoclgft  2945  spcgft  2971  mo2icl  3056  euind  3064  reu6  3066  reuind  3080  sbciegft  3134  dfiin2g  4066  invdisj  4142  elpwunsn  4697  tfindsg  4780  findsg  4812  dff3  5821  zfrep6  5907  fnoprabg  6110  tz7.48-1  6636  odi  6758  r1sdom  7633  kmlem6  7968  kmlem12  7974  zorng  8317  squeeze0  9845  xrsupexmnf  10815  xrinfmexpnf  10816  rexanre  12077  tgcnp  17239  lmcvg  17248  iblcnlem  19547  limcresi  19639  isch3  22592  disjexc  23876  cntmeas  24374  axextdfeq  25178  hbimtg  25187  meran3  25877  waj-ax  25878  lukshef-ax2  25879  imsym1  25882  wl-adnestantALT  25932  nn0prpw  26017  ismrc  26446  pm11.71  27265  a9e2ndeqVD  28362  a9e2ndeqALT  28385  bnj900  28638  bnj1172  28708  bnj1174  28710  bnj1176  28712  ax12olem3aAUX7  28795  ltrnnid  30250
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator