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  ja  186  imim21b  396  jcab  519  pm3.48  963  nanass  1509  nic-ax  1676  nic-axALT  1677  tbw-bijust  1701  merco1  1716  19.23v  1946  19.24  1990  hbsbw  2170  sb4a  2480  2eu6  2653  axi5r  2696  ralrexbidOLD  3108  r19.36v  3184  ceqsal1t  3505  vtoclgft  3541  spcgft  3579  elabgt  3663  mo2icl  3711  euind  3721  reu6  3723  reuind  3750  sbciegft  3816  elpwunsn  4688  dfiin2g  5036  invdisj  5133  ssrel  5783  ssrelOLD  5784  dff3  7102  fnoprabg  7531  tfindsg  7850  findsg  7890  zfrep6  7941  tz7.48-1  8443  odi  8579  r1sdom  9769  kmlem6  10150  kmlem12  10156  zorng  10499  squeeze0  12117  xrsupexmnf  13284  xrinfmexpnf  13285  mptnn0fsuppd  13963  rexanre  15293  pmatcollpw2lem  22279  tgcnp  22757  lmcvg  22766  iblcnlem  25306  limcresi  25402  isch3  30525  disjexc  31855  cntmeas  33255  bnj900  33971  bnj1172  34043  bnj1174  34045  bnj1176  34047  gonarlem  34416  goalrlem  34418  axextdfeq  34800  hbimtg  34809  nn0prpw  35256  meran3  35346  waj-ax  35347  lukshef-ax2  35348  imsym1  35351  bj-peircestab  35477  bj-orim2  35480  bj-andnotim  35514  bj-ssbid2ALT  35588  bj-19.21bit  35616  bj-substax12  35647  bj-ceqsalt0  35812  bj-ceqsalt1  35813  wl-embant  36427  contrd  37013  ax12indi  37862  ltrnnid  39055  ismrc  41487  frege55lem1a  42665  frege55lem1b  42694  frege55lem1c  42715  frege92  42754  pm11.71  43204  exbir  43287  ax6e2ndeqVD  43718  ax6e2ndeqALT  43740  r19.36vf  43873  nn0sumshdiglemA  47353  nn0sumshdiglemB  47354  setrec2mpt  47790