Theorem imim2i 14

Description: Inference adding common antecedents in an implication. (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 13	1

Syntax hints:  ->wi 4

This theorem is referenced by:  imim12i  57  imim3i  59  imim12  97  ja  161  imim21b  367  pm3.48  833  jcab  863  nic-ax  1506  nic-axALT  1507  tbw-bijust  1531  merco1  1546  sbimi  1745  19.24  1758  19.23v  1760  ax12indi  2274  2eu6  2383  axi5r  2427  r19.36v  3005  ceqsalt  3132  vtoclgft  3157  spcgft  3186  mo2icl  3278  euind  3286  reu6  3288  reuind  3303  sbciegft  3358  elpwunsn  4070  dfiin2g  4363  invdisj  4441  dff3  6044  fnoprabg  6403  tfindsg  6695  findsg  6727  zfrep6  6768  tz7.48-1  7127  odi  7247  r1sdom  8213  kmlem6  8556  kmlem12  8562  zorng  8905  squeeze0  10473  xrsupexmnf  11525  xrinfmexpnf  11526  mptnn0fsuppd  12104  reuccats1lem  12705  rexanre  13179  pmatcollpw2lem  19278  tgcnp  19754  lmcvg  19763  bwthOLD  19911  iblcnlem  22195  limcresi  22289  isch3  26159  disjexc  27452  cntmeas  28197  axextdfeq  29230  hbimtg  29239  meran3  29878  waj-ax  29879  lukshef-ax2  29880  imsym1  29883  wl-embantALT  29975  nn0prpw  30141  contrd  30497  ismrc  30633  pm11.71  31303  exbir  33219  ax6e2ndeqVD  33709  ax6e2ndeqALT  33731  bnj900  33987  bnj1172  34057  bnj1174  34059  bnj1176  34061  bj-andnotim  34177  bj-19.21bit  34243  bj-ceqsalt0  34449  bj-ceqsalt1  34450  ltrnnid  35860  rp-fakenanass  37739  frege55lem1a  37893  frege55lem1b  37922  frege55lem1c  37943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7