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 137  impt 141  imbi2i 185  anclb 329  ancrb 330  imdistan 442  pm5.3 446  prth 554  nicodraw 949  19.21 1052  19.24 1079  19.21t 1111  cbv3 1160  cbval 1161  sbimi 1169  ax11indi 1360  mopick 1426  r19.36av 1752  ralcom2 1768  elab3g 1893  mo2icl 1914  reu3 1921  sbciegft 1949  csbiegft 2019  elpwunsn 2902  findsg 3147  tfindsg 3152  zfrep6 3600  fnopabg 3601  dff2 3802  fopab2 3808  cbvfo 3870  tz7.48-1 3941  fnoprabg 3997  odi 4194  kmlem6 4742  kmlem12 4748  suppsr3 5196  pre-axsup 5263  squeeze0 5872  xrsupexmnf 6021  xrinfmexpnf 6022  cau3ir 6852  cau3 6853  cvganz 6861  clm3 7017  clmi2 7025  clm0i 7027  caucvg3 7103  infxpidmlem12 7506  lmcvg2 7871  caun0 7880  chsscm 9033  chcmh 9034  qusp 10430  hgrablkne0 10609

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

Copyright terms: Public domain