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

Theorem ax11i 1633
Description: Inference that has ax-11 1719 (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 218 . . 3  |-  ( ps 
->  ( x  =  y  ->  ph ) )
42, 3alrimih 1557 . 2  |-  ( ps 
->  A. x ( x  =  y  ->  ph )
)
51, 4syl6bi 221 1  |-  ( x  =  y  ->  ( ph  ->  A. x ( x  =  y  ->  ph )
) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178   A.wal 1532
This theorem is referenced by:  ax11wlem  1698
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator