Theorem imim2i 17

Description: Inference adding common antecedents in an implication. Inference associated with imim2 59. Its associated inference is syl 18. (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 15	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  63  imim3i  65  ja  188  imim21b  399  jcab  526  pm3.48  978  nanass  1533  nic-ax  1696  nic-axALT  1697  tbw-bijust  1721  merco1  1736  19.23v  1965  19.24  2014  sb4a  2514  2eu6  2686  axi5r  2729  r19.36v  3193  ceqsal1t  3489  spcgft  3520  vtoclgft  3523  elabgtOLD  3635  mo2icl  3680  euind  3690  reu6  3692  reuind  3719  elpwunsn  4646  dfiin2g  4991  invdisj  5091  zfrep6  5244  ssrel  5760  dff3  7085  fnoprabg  7523  tfindsg  7845  findsg  7882  zfrep6OLD  7940  tz7.48-1  8418  odi  8552  r1sdom  9734  kmlem6  10127  kmlem12  10133  zorng  10476  squeeze0  12109  xrsupexmnf  13322  xrinfmexpnf  13323  mptnn0fsuppd  14025  rexanre  15388  ssdifidlprm  21446  pmatcollpw2lem  22895  tgcnp  23371  lmcvg  23380  iblcnlem  25909  limcresi  26005  isch3  31502  disjexc  32848  cntmeas  34533  bnj900  35234  bnj1172  35306  bnj1174  35308  bnj1176  35310  r1omhfb  35420  r1omhfbregs  35445  gonarlem  35757  goalrlem  35759  axextdfeq  36158  hbimtg  36167  nn0prpw  36696  meran3  36786  waj-ax  36787  lukshef-ax2  36788  imsym1  36791  axnulregtco  36853  mh-setindnd  36910  bj-peircestab  37005  bj-orim2  37010  bj-andnotim  37043  bj-alextruim  37121  bj-ssbid2ALT  37147  bj-19.21bit  37177  bj-substax12  37211  bj-ceqsalt0  37381  bj-ceqsalt1  37382  bj-rep  37570  bj-axreprepsep  37572  wl-embant  38025  contrd  38608  ax12indi  39580  ltrnnid  40772  ismrc  43294  frege55lem1a  44454  frege55lem1b  44483  frege55lem1c  44504  frege92  44543  pm11.71  44971  exbir  45053  ax6e2ndeqVD  45482  ax6e2ndeqALT  45504  r19.36vf  45712  nn0sumshdiglemA  49250  nn0sumshdiglemB  49251  setrec2mpt  50326