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  1642  19.24  1651  19.21h  1743  nfimd  1773  19.21t  1802  ax12olem3  1882  ax11indi  2148  mopick  2218  r19.36av  2701  ceqsalt  2823  vtoclgft  2847  spcgft  2873  mo2icl  2957  euind  2965  reu6  2967  reuind  2981  sbciegft  3034  dfiin2g  3952  invdisj  4028  elpwunsn  4584  tfindsg  4667  findsg  4699  dff3  5689  zfrep6  5764  fnoprabg  5961  tz7.48-1  6471  odi  6593  r1sdom  7462  kmlem6  7797  kmlem12  7803  zorng  8147  squeeze0  9675  xrsupexmnf  10639  xrinfmexpnf  10640  rexanre  11846  tgcnp  16999  lmcvg  17008  iblcnlem  19159  limcresi  19251  isch3  21837  disjexc  23193  cntmeas  23568  axextdfeq  24225  hbimtg  24234  meran3  24924  waj-ax  24925  lukshef-ax2  24926  imsym1  24929  wl-adnestantALT  24979  domrngref  25163  qusp  25645  bwt2  25695  nn0prpw  26342  ismrc  26879  pm11.71  27699  atbiffatnnbalt  27986  cusgrauvtx  28309  bi13imp2  28557  bi12imp3  28558  bi23imp1  28559  bi123imp0  28560  a9e2ndeqVD  29001  a9e2ndeqALT  29024  bnj900  29277  bnj1172  29347  bnj1174  29349  bnj1176  29351  ax12olem3aAUX7  29434  ltrnnid  30947
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator