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  188  imim21b  397  jcab  520  pm3.48  960  nanass  1500  nic-ax  1674  nic-axALT  1675  tbw-bijust  1699  merco1  1714  19.23v  1943  19.24  1992  sb4a  2509  sbimiOLD  2515  sbimiALT  2577  2eu6  2742  axi5r  2785  ralrexbid  3324  r19.36v  3344  ceqsalt  3529  vtoclgft  3555  vtoclgftOLD  3556  spcgft  3589  mo2icl  3707  euind  3717  reu6  3719  reuind  3746  sbciegft  3810  elpwunsn  4623  dfiin2g  4959  invdisj  5052  ssrel  5659  dff3  6868  fnoprabg  7277  tfindsg  7577  findsg  7611  zfrep6  7658  tz7.48-1  8081  odi  8207  r1sdom  9205  kmlem6  9583  kmlem12  9589  zorng  9928  squeeze0  11545  xrsupexmnf  12701  xrinfmexpnf  12702  mptnn0fsuppd  13369  rexanre  14708  pmatcollpw2lem  21387  tgcnp  21863  lmcvg  21872  iblcnlem  24391  limcresi  24485  isch3  29020  disjexc  30345  cntmeas  31487  bnj900  32203  bnj1172  32275  bnj1174  32277  bnj1176  32279  gonarlem  32643  goalrlem  32645  axextdfeq  33044  hbimtg  33053  nn0prpw  33673  meran3  33763  waj-ax  33764  lukshef-ax2  33765  imsym1  33768  bj-peircestab  33890  bj-orim2  33893  bj-andnotim  33924  bj-ssbid2ALT  33998  bj-19.21bit  34026  bj-ceqsalt0  34202  bj-ceqsalt1  34203  wl-embant  34752  contrd  35377  ax12indi  36082  ltrnnid  37274  ismrc  39305  frege55lem1a  40219  frege55lem1b  40248  frege55lem1c  40269  frege92  40308  pm11.71  40736  exbir  40819  ax6e2ndeqVD  41250  ax6e2ndeqALT  41272  r19.36vf  41411  nn0sumshdiglemA  44686  nn0sumshdiglemB  44687