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  ja  189  imim21b  398  jcab  521  pm3.48  961  nanass  1501  nic-ax  1675  nic-axALT  1676  tbw-bijust  1700  merco1  1715  19.23v  1943  19.24  1992  hbsbw  2174  sb4a  2501  sbimiALT  2556  2eu6  2722  axi5r  2765  ralrexbid  3284  r19.36v  3299  ceqsalt  3477  vtoclgft  3504  vtoclgftOLD  3505  spcgft  3538  mo2icl  3656  euind  3666  reu6  3668  reuind  3695  sbciegft  3759  elpwunsn  4584  dfiin2g  4922  invdisj  5017  ssrel  5625  dff3  6847  fnoprabg  7258  tfindsg  7559  findsg  7594  zfrep6  7642  tz7.48-1  8066  odi  8192  r1sdom  9191  kmlem6  9570  kmlem12  9576  zorng  9919  squeeze0  11536  xrsupexmnf  12690  xrinfmexpnf  12691  mptnn0fsuppd  13365  rexanre  14701  pmatcollpw2lem  21385  tgcnp  21861  lmcvg  21870  iblcnlem  24395  limcresi  24491  isch3  29027  disjexc  30359  cntmeas  31593  bnj900  32309  bnj1172  32381  bnj1174  32383  bnj1176  32385  gonarlem  32749  goalrlem  32751  axextdfeq  33150  hbimtg  33159  nn0prpw  33779  meran3  33869  waj-ax  33870  lukshef-ax2  33871  imsym1  33874  bj-peircestab  33996  bj-orim2  33999  bj-andnotim  34030  bj-ssbid2ALT  34104  bj-19.21bit  34132  bj-subst  34163  bj-ceqsalt0  34319  bj-ceqsalt1  34320  wl-embant  34908  contrd  35528  ax12indi  36233  ltrnnid  37425  ismrc  39629  frege55lem1a  40554  frege55lem1b  40583  frege55lem1c  40604  frege92  40643  pm11.71  41088  exbir  41171  ax6e2ndeqVD  41602  ax6e2ndeqALT  41624  r19.36vf  41759  nn0sumshdiglemA  45020  nn0sumshdiglemB  45021
 Copyright terms: Public domain W3C validator