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  30494  disjexc  31824  cntmeas  33224  bnj900  33940  bnj1172  34012  bnj1174  34014  bnj1176  34016  gonarlem  34385  goalrlem  34387  axextdfeq  34769  hbimtg  34778  nn0prpw  35208  meran3  35298  waj-ax  35299  lukshef-ax2  35300  imsym1  35303  bj-peircestab  35429  bj-orim2  35432  bj-andnotim  35466  bj-ssbid2ALT  35540  bj-19.21bit  35568  bj-substax12  35599  bj-ceqsalt0  35764  bj-ceqsalt1  35765  wl-embant  36379  contrd  36965  ax12indi  37814  ltrnnid  39007  ismrc  41439  frege55lem1a  42617  frege55lem1b  42646  frege55lem1c  42667  frege92  42706  pm11.71  43156  exbir  43239  ax6e2ndeqVD  43670  ax6e2ndeqALT  43692  r19.36vf  43825  nn0sumshdiglemA  47305  nn0sumshdiglemB  47306  setrec2mpt  47742