MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax11i Unicode version

Theorem ax11i 1628
Description: Inference that has ax-11 1715 (without  A. y) as its conclusion. Uses only Tarski's FOL axiom schemes. The hypotheses may be eliminable without one or more of these axioms in special cases. Proof similar to Lemma 16 of [Tarski] p. 70. (Contributed by NM, 20-May-2008.)
Hypotheses
Ref Expression
ax11i.1  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
ax11i.2  |-  ( ps 
->  A. x ps )
Assertion
Ref Expression
ax11i  |-  ( x  =  y  ->  ( ph  ->  A. x ( x  =  y  ->  ph )
) )

Proof of Theorem ax11i
StepHypRef Expression
1 ax11i.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
2 ax11i.2 . . 3  |-  ( ps 
->  A. x ps )
31biimprcd 216 . . 3  |-  ( ps 
->  ( x  =  y  ->  ph ) )
42, 3alrimih 1552 . 2  |-  ( ps 
->  A. x ( x  =  y  ->  ph )
)
51, 4syl6bi 219 1  |-  ( x  =  y  ->  ( ph  ->  A. x ( x  =  y  ->  ph )
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wal 1527
This theorem is referenced by:  ax11wlem  1694
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator