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

Step	Hyp	Ref	Expression
1		imim2i.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	a1i 11	. 2 ⊢ (𝜒 → (𝜑 → 𝜓))
3	2	a2i 14	1 ⊢ ((𝜒 → 𝜑) → (𝜒 → 𝜓))

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  175  imim21b  386  jcab  510  pm3.48  946  nanass  1486  nanassOLD  1487  nic-ax  1636  nic-axALT  1637  tbw-bijust  1661  merco1  1676  19.23v  1901  19.24  1942  sb4a  2429  sbimiOLD  2435  sbimiALT  2504  2eu6  2688  axi5r  2740  r19.36v  3283  ceqsalt  3448  vtoclgft  3474  spcgft  3506  mo2icl  3621  euind  3629  reu6  3631  reuind  3655  sbciegft  3714  elpwunsn  4496  dfiin2g  4828  invdisj  4916  ssrel  5508  dff3  6691  fnoprabg  7093  tfindsg  7393  findsg  7426  zfrep6  7470  tz7.48-1  7884  odi  8008  r1sdom  8999  kmlem6  9377  kmlem12  9383  zorng  9726  squeeze0  11346  xrsupexmnf  12517  xrinfmexpnf  12518  mptnn0fsuppd  13184  reuccats1lemOLD  13923  rexanre  14570  pmatcollpw2lem  21092  tgcnp  21568  lmcvg  21577  iblcnlem  24095  limcresi  24189  isch3  28800  disjexc  30112  cntmeas  31130  bnj900  31848  bnj1172  31918  bnj1174  31920  bnj1176  31922  axextdfeq  32563  hbimtg  32572  nn0prpw  33192  meran3  33281  waj-ax  33282  lukshef-ax2  33283  imsym1  33286  bj-orim2  33408  bj-andnotim  33439  bj-ssbid2ALT  33505  bj-19.21bit  33534  bj-ceqsalt0  33693  bj-ceqsalt1  33694  wl-embant  34191  contrd  34819  ax12indi  35525  ltrnnid  36717  ismrc  38693  frege55lem1a  39575  frege55lem1b  39604  frege55lem1c  39625  frege92  39664  pm11.71  40146  exbir  40231  ax6e2ndeqVD  40662  ax6e2ndeqALT  40684  r19.36vf  40827  nn0sumshdiglemA  44048  nn0sumshdiglemB  44049