Theorem a2i 9

Description: Inference derived from axiom ax-2 5.

Hypothesis

Ref	Expression
a2i.1	|- (ph -> (ps -> ch))

Assertion

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

Proof of Theorem a2i

Step	Hyp	Ref	Expression
1		a2i.1	. 2 |- (ph -> (ps -> ch))
2		ax-2 5	. 2 |- ((ph -> (ps -> ch)) -> ((ph -> ps) -> (ph -> ch)))
3	1, 2	ax-mp 7	1 |- ((ph -> ps) -> (ph -> ch))

Syntax hints:   -> wi 3

This theorem is referenced by:  syl 10  com12 11  imim2i 17  mpd 26  sylcom 51  pm2.43 63  pm2.18 81  pm2.65 134  ancl 294  ancr 295  anc2l 300  anc2r 301  hbim1 1099  r19.20i 1696  ceqsalg 1816  elabgt 1886  tfi 3116  dfom3 4602  peano2nn 5883  climserzle 7083  caucvglem6 7098  isummulc1ALT 7148  caun0 7880  pjnormss 10007

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

Copyright terms: Public domain