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  187  imim21b  395  jcab  522  pm3.48  971  nanass  1517  nic-ax  1680  nic-axALT  1681  tbw-bijust  1705  merco1  1720  19.23v  1949  19.24  1998  sb4a  2488  2eu6  2661  axi5r  2704  r19.36v  3168  ceqsal1t  3465  spcgft  3497  vtoclgft  3500  elabgtOLD  3618  mo2icl  3662  euind  3672  reu6  3674  reuind  3701  elpwunsn  4623  dfiin2g  4967  invdisj  5065  zfrep6  5218  ssrel  5733  dff3  7048  fnoprabg  7486  tfindsg  7808  findsg  7844  zfrep6OLD  7904  tz7.48-1  8379  odi  8511  r1sdom  9696  kmlem6  10076  kmlem12  10082  zorng  10424  squeeze0  12057  xrsupexmnf  13255  xrinfmexpnf  13256  mptnn0fsuppd  13958  rexanre  15307  pmatcollpw2lem  22767  tgcnp  23243  lmcvg  23252  iblcnlem  25781  limcresi  25877  isch3  31337  disjexc  32689  ssdifidlprm  33548  cntmeas  34417  bnj900  35118  bnj1172  35190  bnj1174  35192  bnj1176  35194  r1omhfb  35300  r1omhfbregs  35325  gonarlem  35629  goalrlem  35631  axextdfeq  36030  hbimtg  36039  nn0prpw  36558  meran3  36648  waj-ax  36649  lukshef-ax2  36650  imsym1  36653  axnulregtco  36715  mh-setindnd  36772  bj-peircestab  36868  bj-orim2  36873  bj-andnotim  36906  bj-alextruim  36984  bj-ssbid2ALT  37010  bj-19.21bit  37040  bj-substax12  37074  bj-ceqsalt0  37244  bj-ceqsalt1  37245  bj-rep  37433  bj-axreprepsep  37435  wl-embant  37888  contrd  38471  ax12indi  39443  ltrnnid  40635  ismrc  43157  frege55lem1a  44317  frege55lem1b  44346  frege55lem1c  44367  frege92  44406  pm11.71  44848  exbir  44930  ax6e2ndeqVD  45359  ax6e2ndeqALT  45381  r19.36vf  45590  nn0sumshdiglemA  49117  nn0sumshdiglemB  49118  setrec2mpt  50194