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  966  nanass  1512  nic-ax  1675  nic-axALT  1676  tbw-bijust  1700  merco1  1715  19.23v  1944  19.24  1993  hbsbwOLD  2178  sb4a  2485  2eu6  2658  axi5r  2701  r19.36v  3166  ceqsal1t  3463  spcgft  3495  vtoclgft  3498  elabgtOLD  3616  elabgtOLDOLD  3617  mo2icl  3661  euind  3671  reu6  3673  reuind  3700  sbciegftOLD  3767  elpwunsn  4629  dfiin2g  4974  invdisj  5072  zfrep6  5224  ssrel  5732  dff3  7046  fnoprabg  7483  tfindsg  7805  findsg  7841  zfrep6OLD  7901  tz7.48-1  8375  odi  8507  r1sdom  9689  kmlem6  10069  kmlem12  10075  zorng  10417  squeeze0  12050  xrsupexmnf  13248  xrinfmexpnf  13249  mptnn0fsuppd  13951  rexanre  15300  pmatcollpw2lem  22752  tgcnp  23228  lmcvg  23237  iblcnlem  25766  limcresi  25862  isch3  31327  disjexc  32678  ssdifidlprm  33533  cntmeas  34386  bnj900  35087  bnj1172  35159  bnj1174  35161  bnj1176  35163  r1omhfb  35272  r1omhfbregs  35297  gonarlem  35592  goalrlem  35594  axextdfeq  35993  hbimtg  36002  nn0prpw  36521  meran3  36611  waj-ax  36612  lukshef-ax2  36613  imsym1  36616  axnulregtco  36678  mh-setindnd  36735  bj-peircestab  36831  bj-orim2  36836  bj-andnotim  36869  bj-alextruim  36947  bj-ssbid2ALT  36973  bj-19.21bit  37003  bj-substax12  37037  bj-ceqsalt0  37207  bj-ceqsalt1  37208  bj-rep  37396  bj-axreprepsep  37398  wl-embant  37849  contrd  38432  ax12indi  39404  ltrnnid  40596  ismrc  43147  frege55lem1a  44311  frege55lem1b  44340  frege55lem1c  44361  frege92  44400  pm11.71  44842  exbir  44924  ax6e2ndeqVD  45353  ax6e2ndeqALT  45375  r19.36vf  45584  nn0sumshdiglemA  49107  nn0sumshdiglemB  49108  setrec2mpt  50184