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 1101  r19.20i 1701  ceqsalg 1821  elabgt 1891  tfi 3121  dfom3 4610  peano2nn 5891  climserzle 7091  caucvglem6 7106  isummulc1ALT 7156  caun0 7896  pjnormss 10034

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

Copyright terms: Public domain