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  2484  2eu6  2657  axi5r  2700  r19.36v  3164  ceqsal1t  3473  spcgft  3506  vtoclgft  3509  elabgtOLD  3627  elabgtOLDOLD  3628  mo2icl  3672  euind  3682  reu6  3684  reuind  3711  sbciegftOLD  3778  elpwunsn  4641  dfiin2g  4986  invdisj  5084  ssrel  5732  dff3  7045  fnoprabg  7481  tfindsg  7803  findsg  7839  zfrep6  7899  tz7.48-1  8374  odi  8506  r1sdom  9686  kmlem6  10066  kmlem12  10072  zorng  10414  squeeze0  12045  xrsupexmnf  13220  xrinfmexpnf  13221  mptnn0fsuppd  13921  rexanre  15270  pmatcollpw2lem  22721  tgcnp  23197  lmcvg  23206  iblcnlem  25746  limcresi  25842  isch3  31316  disjexc  32668  ssdifidlprm  33539  cntmeas  34383  bnj900  35085  bnj1172  35157  bnj1174  35159  bnj1176  35161  r1omhfb  35268  r1omhfbregs  35293  gonarlem  35588  goalrlem  35590  axextdfeq  35989  hbimtg  35998  nn0prpw  36517  meran3  36607  waj-ax  36608  lukshef-ax2  36609  imsym1  36612  mh-setindnd  36667  bj-peircestab  36753  bj-orim2  36756  bj-andnotim  36788  bj-ssbid2ALT  36864  bj-19.21bit  36891  bj-substax12  36922  bj-ceqsalt0  37085  bj-ceqsalt1  37086  wl-embant  37711  contrd  38294  ax12indi  39200  ltrnnid  40392  ismrc  42939  frege55lem1a  44103  frege55lem1b  44132  frege55lem1c  44153  frege92  44192  pm11.71  44634  exbir  44716  ax6e2ndeqVD  45145  ax6e2ndeqALT  45167  r19.36vf  45376  nn0sumshdiglemA  48861  nn0sumshdiglemB  48862  setrec2mpt  49938