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

Theorem ax11indi 2196
 Description: Induction step for constructing a substitution instance of ax-11o 2141 without using ax-11o 2141. Implication case. (Contributed by NM, 21-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
ax11indn.1 x x = y → (x = y → (φx(x = yφ))))
ax11indi.2 x x = y → (x = y → (ψx(x = yψ))))
Assertion
Ref Expression
ax11indi x x = y → (x = y → ((φψ) → x(x = y → (φψ)))))

Proof of Theorem ax11indi
StepHypRef Expression
1 ax11indn.1 . . . . . 6 x x = y → (x = y → (φx(x = yφ))))
21ax11indn 2195 . . . . 5 x x = y → (x = y → (¬ φx(x = y → ¬ φ))))
32imp 418 . . . 4 ((¬ x x = y x = y) → (¬ φx(x = y → ¬ φ)))
4 pm2.21 100 . . . . . 6 φ → (φψ))
54imim2i 13 . . . . 5 ((x = y → ¬ φ) → (x = y → (φψ)))
65alimi 1559 . . . 4 (x(x = y → ¬ φ) → x(x = y → (φψ)))
73, 6syl6 29 . . 3 ((¬ x x = y x = y) → (¬ φx(x = y → (φψ))))
8 ax11indi.2 . . . . 5 x x = y → (x = y → (ψx(x = yψ))))
98imp 418 . . . 4 ((¬ x x = y x = y) → (ψx(x = yψ)))
10 ax-1 6 . . . . . 6 (ψ → (φψ))
1110imim2i 13 . . . . 5 ((x = yψ) → (x = y → (φψ)))
1211alimi 1559 . . . 4 (x(x = yψ) → x(x = y → (φψ)))
139, 12syl6 29 . . 3 ((¬ x x = y x = y) → (ψx(x = y → (φψ))))
147, 13jad 154 . 2 ((¬ x x = y x = y) → ((φψ) → x(x = y → (φψ))))
1514ex 423 1 x x = y → (x = y → ((φψ) → x(x = y → (φψ)))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 358  ∀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-an 360  df-ex 1542 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator