Theorem imim2i 16

Description: Inference adding common antecedents in an implication. Inference associated with imim2 56. 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  60  imim3i  62  imim12  103  ja  172  imim21b  381  pm3.48  874  jcab  903  nic-ax  1589  nic-axALT  1590  tbw-bijust  1614  merco1  1629  sbimi  1873  19.24  1887  19.23v  1889  2eu6  2546  axi5r  2582  r19.36v  3066  ceqsalt  3201  vtoclgft  3227  vtoclgftOLD  3228  spcgft  3258  mo2icl  3352  euind  3360  reu6  3362  reuind  3378  sbciegft  3433  elpwunsn  4171  dfiin2g  4489  invdisj  4571  ssrel  5130  dff3  6280  fnoprabg  6659  tfindsg  6952  findsg  6985  zfrep6  7027  tz7.48-1  7425  odi  7546  r1sdom  8520  kmlem6  8860  kmlem12  8866  zorng  9209  squeeze0  10805  xrsupexmnf  12007  xrinfmexpnf  12008  mptnn0fsuppd  12660  reuccats1lem  13331  rexanre  13934  pmatcollpw2lem  20401  tgcnp  20867  lmcvg  20876  iblcnlem  23361  limcresi  23455  isch3  27482  disjexc  28788  cntmeas  29616  bnj900  30253  bnj1172  30323  bnj1174  30325  bnj1176  30327  axextdfeq  30947  hbimtg  30956  nn0prpw  31488  meran3  31582  waj-ax  31583  lukshef-ax2  31584  imsym1  31587  bj-orim2  31711  bj-currypeirce  31714  bj-andnotim  31746  bj-ssbequ2  31832  bj-ssbid2ALT  31835  bj-19.21bit  31867  bj-ceqsalt0  32067  bj-ceqsalt1  32068  wl-nf2-nf  32464  wl-embant  32472  contrd  33069  ax12indi  33247  ltrnnid  34440  ismrc  36282  rp-fakenanass  36879  frege55lem1a  37180  frege55lem1b  37209  frege55lem1c  37230  frege92  37269  pm11.71  37619  exbir  37705  ax6e2ndeqVD  38167  ax6e2ndeqALT  38189  nn0sumshdiglemA  42211  nn0sumshdiglemB  42212