Theorem hbimOLD 1818

Description: Obsolete proof of hbim 1817 as of 1-Jan-2018. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 3-Mar-2008.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses

Ref	Expression
hbim.1	|- (ph -> A.xph)
hbim.2	|- (ps -> A.xps)

Assertion

Ref	Expression
hbimOLD	|- ((ph -> ps) -> A.x(ph -> ps))

Proof of Theorem hbimOLD

Step	Hyp	Ref	Expression
1		hbim.1	. . . 4 |- (ph -> A.xph)
2	1	hbn 1776	. . 3 |- (-. ph -> A.x -. ph)
3		pm2.21 100	. . 3 |- (-. ph -> (ph -> ps))
4	2, 3	alrimih 1565	. 2 |- (-. ph -> A.x(ph -> ps))
5		hbim.2	. . 3 |- (ps -> A.xps)
6		ax-1 6	. . 3 |- (ps -> (ph -> ps))
7	5, 6	alrimih 1565	. 2 |- (ps -> A.x(ph -> ps))
8	4, 7	ja 153	1 |- ((ph -> ps) -> A.x(ph -> ps))

Syntax hints:  -. wn 3   -> wi 4  A.wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-ex 1542

This theorem is referenced by: (None)