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  1510  nic-ax  1673  nic-axALT  1674  tbw-bijust  1698  merco1  1713  19.23v  1942  19.24  1991  hbsbwOLD  2173  sb4a  2478  2eu6  2650  axi5r  2693  r19.36v  3157  ceqsal1t  3471  spcgft  3506  vtoclgft  3509  elabgtOLD  3630  elabgtOLDOLD  3631  mo2icl  3676  euind  3686  reu6  3688  reuind  3715  sbciegftOLD  3782  elpwunsn  4638  dfiin2g  4984  invdisj  5081  ssrel  5730  dff3  7038  fnoprabg  7476  tfindsg  7801  findsg  7837  zfrep6  7897  tz7.48-1  8372  odi  8504  r1sdom  9689  kmlem6  10069  kmlem12  10075  zorng  10417  squeeze0  12046  xrsupexmnf  13225  xrinfmexpnf  13226  mptnn0fsuppd  13923  rexanre  15272  pmatcollpw2lem  22680  tgcnp  23156  lmcvg  23165  iblcnlem  25706  limcresi  25802  isch3  31203  disjexc  32555  ssdifidlprm  33408  cntmeas  34195  bnj900  34898  bnj1172  34970  bnj1174  34972  bnj1176  34974  gonarlem  35369  goalrlem  35371  axextdfeq  35773  hbimtg  35782  nn0prpw  36299  meran3  36389  waj-ax  36390  lukshef-ax2  36391  imsym1  36394  bj-peircestab  36529  bj-orim2  36532  bj-andnotim  36564  bj-ssbid2ALT  36639  bj-19.21bit  36666  bj-substax12  36697  bj-ceqsalt0  36860  bj-ceqsalt1  36861  wl-embant  37486  contrd  38079  ax12indi  38925  ltrnnid  40118  ismrc  42677  frege55lem1a  43842  frege55lem1b  43871  frege55lem1c  43892  frege92  43931  pm11.71  44373  exbir  44456  ax6e2ndeqVD  44885  ax6e2ndeqALT  44907  r19.36vf  45117  nn0sumshdiglemA  48608  nn0sumshdiglemB  48609  setrec2mpt  49686