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 556  nicodraw 952  19.21 1056  19.24 1083  19.21t 1115  cbv3 1164  cbval 1165  sbimi 1173  ax11indi 1367  mopick 1433  r19.36av 1760  ralcom2 1776  elab3g 1902  mo2icl 1923  reu3 1931  sbciegft 1959  csbiegft 2029  elpwunsn 2912  findsg 3157  tfindsg 3162  zfrep6 3614  fnopabg 3615  dff2 3817  fopab2 3823  cbvfo 3885  tz7.48-1 3956  fnoprabg 4012  odi 4210  kmlem6 4770  kmlem12 4776  suppsr3 5224  pre-axsup 5291  squeeze0 5924  xrsupexmnf 6074  xrinfmexpnf 6075  cau3ir 6915  cau3 6916  cvganz 6924  clm3 7079  clmi2 7087  clm0i 7089  caucvg3 7167  infxpidmlem12 7563  lmcvg2 7933  caun0 7945  chsscm 9112  chcmh 9113  qusp 10555  hgrablkne0 10773

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

Copyright terms: Public domain