Theorem a2i 10

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:  imim2i 11  sylOLD 13  com12 14  mpd 29  sylcom 62  pm2.43 77  pm2.18 96  pm2.65 148  ancl 316  ancr 317  anc2l 322  anc2r 323  hbim1 1296  ralimia 2000  ceqsalg 2147  ceqsalgOLD 2148  elabgt 2233  elabgtOLD 2234  tfi 3748  dfom3 5546  peano2nn 6913  climserzlei 8202  caucvglem6 8217  isummulc1iALT 8269  caun0 9018  pjnormssi 11532  bnj1107 12715  waj-ax 13968  rcla4t 16089

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

Copyright terms: Public domain