Theorem imim2i 11

Description: Inference adding common antecedents in an implication.

Hypothesis

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

Assertion

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

Proof of Theorem imim2i

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

Syntax hints:   -> wi 3

This theorem is referenced by:  syl 12  imim12i 21  imim12iOLD 22  imim3i 23  syl6 25  syl8 27  con1 108  con3 110  ja 152  impt 158  imbi2i 202  anclb 356  ancrb 357  imdistan 490  pm5.3OLD 495  prth 615  meredith 1200  nic-ax 1239  nic-axALT 1240  exbir 1285  com3rgbi 1293  19.21 1403  19.24 1434  19.21t 1473  cbv3 1525  cbvalOLD 1528  sbimi 1537  sbf3t 1619  ax11indi 1758  mopick 1833  r19.36av 2232  ralcom2 2244  ralcom2OLD 2245  elab3gOLDOLD 2411  mo2icl 2434  euind 2439  reu6 2443  reuind 2450  sbciegft 2482  csbiegft 2573  dfiin2g 3286  elpwunsn 3856  tfindsg 3944  findsg 3980  zfrep6 4545  fnopabg 4546  dff3 4790  fopab2 4796  cbvfo 4861  fnoprabg 4941  tz7.48-1 5165  odi 5258  pm2.43bgbi 5835  pm2.43cbi 5836  kmlem6 5932  kmlem12 5938  suppsr3 6376  pre-axsup 6444  squeeze0 7107  xrsupexmnf 7283  xrinfmexpnf 7284  cau3iri 8167  cau3i 8168  cvganz 8176  clm3i 8339  clmi2i 8347  clm0ii 8349  caucvg3i 8427  infxpidmlem12 8832  lmcvg2 9211  caun0 9223  gagrpid 9458  chsscmi 10745  chcmhi 10746  bnj1126 12932  bnj1167 12959  bnj849 13318  bnj900 13325  bnj1007 13372  bnj1172 13440  bnj1174 13442  imim21b 13597  r19.21 13818  axextdfeq 13864  hbimtg 13873  hbaltg 13874  tbw-bijust 14165  merco1 14180  meran3 14237  waj-ax 14238  lukshef-ax2 14239  arg-ax 14240  imsym1 14242  domrngref 14364  fopab2g 14485  qusp 14908  bwt2 14960  dfiin2gOLD 15356  neibastop2 15523  limfilcf 15587  fcluscf 15612  hgrablkne0 16295  pm11.71 16354  euunianOLD 16396  cla4gft 16406  smores 16446

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

Copyright terms: Public domain