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  896  jcab  925  nic-ax  1638  nic-axALT  1639  tbw-bijust  1663  merco1  1678  19.23v  1911  sbimi  1943  19.24  1957  19.23vOLD  1959  2eu6  2587  axi5r  2623  r19.36v  3114  ceqsalt  3259  vtoclgft  3285  vtoclgftOLD  3286  spcgft  3316  mo2icl  3418  euind  3426  reu6  3428  reuind  3444  sbciegft  3499  elpwunsn  4256  dfiin2g  4585  invdisj  4670  ssrel  5241  dff3  6412  fnoprabg  6803  tfindsg  7102  findsg  7135  zfrep6  7176  tz7.48-1  7583  odi  7704  r1sdom  8675  kmlem6  9015  kmlem12  9021  zorng  9364  squeeze0  10964  xrsupexmnf  12173  xrinfmexpnf  12174  mptnn0fsuppd  12838  reuccats1lem  13525  rexanre  14130  pmatcollpw2lem  20630  tgcnp  21105  lmcvg  21114  iblcnlem  23600  limcresi  23694  isch3  28226  disjexc  29532  cntmeas  30417  bnj900  31125  bnj1172  31195  bnj1174  31197  bnj1176  31199  axextdfeq  31827  hbimtg  31836  nn0prpw  32443  meran3  32537  waj-ax  32538  lukshef-ax2  32539  imsym1  32542  bj-orim2  32666  bj-currypeirce  32669  bj-andnotim  32698  bj-ssbequ2  32768  bj-ssbid2ALT  32771  bj-19.21bit  32805  bj-ceqsalt0  32998  bj-ceqsalt1  32999  wl-embant  33423  contrd  34029  ax12indi  34548  ltrnnid  35740  ismrc  37581  rp-fakenanass  38177  frege55lem1a  38477  frege55lem1b  38506  frege55lem1c  38527  frege92  38566  pm11.71  38914  exbir  39001  ax6e2ndeqVD  39459  ax6e2ndeqALT  39481  r19.36vf  39638  nn0sumshdiglemA  42738  nn0sumshdiglemB  42739
 Copyright terms: Public domain W3C validator