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

Theorem imim2i 16
Description: Inference adding common antecedents in an implication. Inference associated with imim2 58. Its associated inference is syl 17. (Contributed by NM, 28-Dec-1992.)
Hypothesis
Ref Expression
imim2i.1 (𝜑𝜓)
Assertion
Ref Expression
imim2i ((𝜒𝜑) → (𝜒𝜓))

Proof of Theorem imim2i
StepHypRef Expression
1 imim2i.1 . . 3 (𝜑𝜓)
21a1i 11 . 2 (𝜒 → (𝜑𝜓))
32a2i 14 1 ((𝜒𝜑) → (𝜒𝜓))
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  62  imim3i  64  imim12  105  ja  173  imim21b  381  pm3.48  914  jcab  943  nic-ax  1739  nic-axALT  1740  tbw-bijust  1764  merco1  1779  19.23v  2012  sbimi  2044  19.24  2058  19.23vOLD  2060  2eu6  2688  axi5r  2724  r19.36v  3215  ceqsalt  3360  vtoclgft  3386  vtoclgftOLD  3387  spcgft  3417  mo2icl  3518  euind  3526  reu6  3528  reuind  3544  sbciegft  3599  elpwunsn  4360  dfiin2g  4697  invdisj  4782  ssrel  5356  dff3  6527  fnoprabg  6918  tfindsg  7217  findsg  7250  zfrep6  7291  tz7.48-1  7699  odi  7820  r1sdom  8802  kmlem6  9161  kmlem12  9167  zorng  9510  squeeze0  11110  xrsupexmnf  12320  xrinfmexpnf  12321  mptnn0fsuppd  12984  reuccats1lem  13671  rexanre  14277  pmatcollpw2lem  20776  tgcnp  21251  lmcvg  21260  iblcnlem  23746  limcresi  23840  isch3  28399  disjexc  29705  cntmeas  30590  bnj900  31298  bnj1172  31368  bnj1174  31370  bnj1176  31372  axextdfeq  32000  hbimtg  32009  nn0prpw  32616  meran3  32710  waj-ax  32711  lukshef-ax2  32712  imsym1  32715  bj-orim2  32839  bj-currypeirce  32842  bj-andnotim  32871  bj-ssbequ2  32941  bj-ssbid2ALT  32944  bj-19.21bit  32978  bj-ceqsalt0  33171  bj-ceqsalt1  33172  wl-embant  33598  contrd  34204  ax12indi  34725  ltrnnid  35917  ismrc  37758  rp-fakenanass  38354  frege55lem1a  38654  frege55lem1b  38683  frege55lem1c  38704  frege92  38743  pm11.71  39091  exbir  39178  ax6e2ndeqVD  39636  ax6e2ndeqALT  39658  r19.36vf  39815  nn0sumshdiglemA  42915  nn0sumshdiglemB  42916
  Copyright terms: Public domain W3C validator