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 555  nicodraw 950  19.21 1054  19.24 1081  19.21t 1113  cbv3 1162  cbval 1163  sbimi 1171  ax11indi 1365  mopick 1431  r19.36av 1757  ralcom2 1773  elab3g 1898  mo2icl 1919  reu3 1927  sbciegft 1955  csbiegft 2025  elpwunsn 2907  findsg 3152  tfindsg 3157  zfrep6 3606  fnopabg 3607  dff2 3808  fopab2 3814  cbvfo 3876  tz7.48-1 3947  fnoprabg 4003  odi 4200  kmlem6 4750  kmlem12 4756  suppsr3 5204  pre-axsup 5271  squeeze0 5880  xrsupexmnf 6029  xrinfmexpnf 6030  cau3ir 6860  cau3 6861  cvganz 6869  clm3 7025  clmi2 7033  clm0i 7035  caucvg3 7111  infxpidmlem12 7514  lmcvg2 7885  caun0 7896  chsscm 9051  chcmh 9052  qusp 10466  hgrablkne0 10645

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

Copyright terms: Public domain