New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  hbimdOLD GIF version

Theorem hbimdOLD 1816
 Description: Obsolete proof of hbimd 1815 as of 16-Dec-2017. (Contributed by NM, 1-Jan-2002.) (New usage is discouraged.)
Hypotheses
Ref Expression
hbimd.1 (φxφ)
hbimd.2 (φ → (ψxψ))
hbimd.3 (φ → (χxχ))
Assertion
Ref Expression
hbimdOLD (φ → ((ψχ) → x(ψχ)))

Proof of Theorem hbimdOLD
StepHypRef Expression
1 hbimd.1 . . . . 5 (φxφ)
2 hbimd.2 . . . . 5 (φ → (ψxψ))
31, 2alrimih 1565 . . . 4 (φx(ψxψ))
4 sp 1747 . . . . . 6 (xψψ)
5 hbn1 1730 . . . . . 6 xψx ¬ xψ)
64, 5nsyl4 134 . . . . 5 x ¬ xψψ)
76con1i 121 . . . 4 ψx ¬ xψ)
8 con3 126 . . . . 5 ((ψxψ) → (¬ xψ → ¬ ψ))
98al2imi 1561 . . . 4 (x(ψxψ) → (x ¬ xψx ¬ ψ))
103, 7, 9syl2im 34 . . 3 (φ → (¬ ψx ¬ ψ))
11 pm2.21 100 . . . 4 ψ → (ψχ))
1211alimi 1559 . . 3 (x ¬ ψx(ψχ))
1310, 12syl6 29 . 2 (φ → (¬ ψx(ψχ)))
14 hbimd.3 . . 3 (φ → (χxχ))
15 ax-1 5 . . . 4 (χ → (ψχ))
1615alimi 1559 . . 3 (xχx(ψχ))
1714, 16syl6 29 . 2 (φ → (χx(ψχ)))
1813, 17jad 154 1 (φ → ((ψχ) → x(ψχ)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1540 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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)
 Copyright terms: Public domain W3C validator