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 84  pm2.65 140  ancl 301  ancr 302  anc2l 307  anc2r 308  hbim1 1144  r19.20i 1751  ceqsalg 1872  elabgt 1942  tfi 3183  dfom3 4692  peano2nn 5995  climserzlei 7237  caucvglem6 7252  isummulc1iALT 7303  caun0 8030  pjnormssi 10179

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

Copyright terms: Public domain