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  189  imim21b  398  jcab  521  pm3.48  964  nanass  1506  nic-ax  1681  nic-axALT  1682  tbw-bijust  1706  merco1  1721  19.23v  1950  19.24  1995  hbsbw  2175  sb4a  2483  2eu6  2657  axi5r  2700  ralrexbid  3231  r19.36v  3246  ceqsalt  3428  vtoclgft  3458  spcgft  3493  elabgt  3570  mo2icl  3616  euind  3626  reu6  3628  reuind  3655  sbciegft  3721  elpwunsn  4585  dfiin2g  4927  invdisj  5023  ssrel  5639  dff3  6897  fnoprabg  7311  tfindsg  7617  findsg  7655  zfrep6  7706  tz7.48-1  8157  odi  8285  r1sdom  9355  kmlem6  9734  kmlem12  9740  zorng  10083  squeeze0  11700  xrsupexmnf  12860  xrinfmexpnf  12861  mptnn0fsuppd  13536  rexanre  14875  pmatcollpw2lem  21628  tgcnp  22104  lmcvg  22113  iblcnlem  24640  limcresi  24736  isch3  29276  disjexc  30605  cntmeas  31860  bnj900  32576  bnj1172  32648  bnj1174  32650  bnj1176  32652  gonarlem  33023  goalrlem  33025  axextdfeq  33443  hbimtg  33452  nn0prpw  34198  meran3  34288  waj-ax  34289  lukshef-ax2  34290  imsym1  34293  bj-peircestab  34419  bj-orim2  34422  bj-andnotim  34456  bj-ssbid2ALT  34530  bj-19.21bit  34558  bj-substax12  34589  bj-ceqsalt0  34756  bj-ceqsalt1  34757  wl-embant  35355  contrd  35941  ax12indi  36644  ltrnnid  37836  ismrc  40167  frege55lem1a  41092  frege55lem1b  41121  frege55lem1c  41142  frege92  41181  pm11.71  41629  exbir  41712  ax6e2ndeqVD  42143  ax6e2ndeqALT  42165  r19.36vf  42299  nn0sumshdiglemA  45581  nn0sumshdiglemB  45582