Theorem imim2i 17

Description: Inference adding common antecedents in an implication.

Hypothesis

Ref	Expression
imim1i.1	|- (ph -> ps)

Assertion

Ref	Expression
imim2i	|- ((ch -> ph) -> (ch -> ps))

Proof of Theorem imim2i

Step	Hyp	Ref	Expression
1		imim1i.1	. . 3 |- (ph -> ps)
2	1	a1i 8	. 2 |- (ch -> (ph -> ps))
3	2	a2i 9	1 |- ((ch -> ph) -> (ch -> ps))

Syntax hints:   -> wi 3

This theorem is referenced by:  imim12i 18  imim3i 19  syl6 22  syl8 24  con1 92  con3 94  ja 135  impt 139  imbi2i 183  anclb 327  ancrb 328  imdistan 444  pm5.3 448  prth 559  nic-ax 969  nic-axALT 970  19.21 1092  19.24 1119  19.21t 1151  cbv3 1201  cbval 1202  sbimi 1210  sbf3t 1285  ax11indi 1406  mopick 1472  r19.36av 1806  ralcom2 1822  elab3g 1948  mo2icl 1969  reu3 1977  sbciegft 2007  csbiegft 2081  elpwunsn 3135  tfindsg 3213  findsg 3245  zfrep6 3721  fnopabg 3722  dff3 3931  fopab2 3937  cbvfo 3999  fnoprabg 4072  tz7.48-1 4257  odi 4346  kmlem6 4916  kmlem12 4922  suppsr3 5378  pre-axsup 5445  squeeze0 6069  xrsupexmnf 6242  xrinfmexpnf 6243  cau3iri 7118  cau3i 7119  cvganz 7127  clm3i 7282  clmi2i 7290  clm0ii 7292  caucvg3i 7370  infxpidmlem12 7775  lmcvg2 8144  caun0 8156  chsscmi 9388  chcmhi 9389  domrngref 10764  qusp 11068  bwt2 11123  dfiin2g 11400  neibastop2 11584  limfilcf 11683  fcluscf 11724  gagrpid 11780  hgrablkne0 12199

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

Copyright terms: Public domain