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  394  jcab  517  pm3.48  965  nanass  1511  nic-ax  1674  nic-axALT  1675  tbw-bijust  1699  merco1  1714  19.23v  1943  19.24  1992  hbsbwOLD  2177  sb4a  2482  2eu6  2654  axi5r  2697  r19.36v  3161  ceqsal1t  3470  spcgft  3503  vtoclgft  3506  elabgtOLD  3624  elabgtOLDOLD  3625  mo2icl  3669  euind  3679  reu6  3681  reuind  3708  sbciegftOLD  3775  elpwunsn  4636  dfiin2g  4981  invdisj  5079  ssrel  5727  dff3  7039  fnoprabg  7475  tfindsg  7797  findsg  7833  zfrep6  7893  tz7.48-1  8368  odi  8500  r1sdom  9674  kmlem6  10054  kmlem12  10060  zorng  10402  squeeze0  12032  xrsupexmnf  13206  xrinfmexpnf  13207  mptnn0fsuppd  13907  rexanre  15256  pmatcollpw2lem  22693  tgcnp  23169  lmcvg  23178  iblcnlem  25718  limcresi  25814  isch3  31223  disjexc  32575  ssdifidlprm  33430  cntmeas  34260  bnj900  34962  bnj1172  35034  bnj1174  35036  bnj1176  35038  r1omhfb  35144  r1omhfbregs  35154  gonarlem  35459  goalrlem  35461  axextdfeq  35860  hbimtg  35869  nn0prpw  36388  meran3  36478  waj-ax  36479  lukshef-ax2  36480  imsym1  36483  bj-peircestab  36618  bj-orim2  36621  bj-andnotim  36653  bj-ssbid2ALT  36728  bj-19.21bit  36755  bj-substax12  36786  bj-ceqsalt0  36949  bj-ceqsalt1  36950  wl-embant  37575  contrd  38158  ax12indi  39064  ltrnnid  40256  ismrc  42819  frege55lem1a  43984  frege55lem1b  44013  frege55lem1c  44034  frege92  44073  pm11.71  44515  exbir  44597  ax6e2ndeqVD  45026  ax6e2ndeqALT  45048  r19.36vf  45258  nn0sumshdiglemA  48745  nn0sumshdiglemB  48746  setrec2mpt  49823