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

Theorem ax12i 1764
Description: Inference that has ax-12 1880 (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
ax12i.1  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
ax12i.2  |-  ( ps 
->  A. x ps )
Assertion
Ref Expression
ax12i  |-  ( x  =  y  ->  ( ph  ->  A. x ( x  =  y  ->  ph )
) )

Proof of Theorem ax12i
StepHypRef Expression
1 ax12i.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
2 ax12i.2 . . 3  |-  ( ps 
->  A. x ps )
31biimprcd 227 . . 3  |-  ( ps 
->  ( x  =  y  ->  ph ) )
42, 3alrimih 1665 . 2  |-  ( ps 
->  A. x ( x  =  y  ->  ph )
)
51, 4syl6bi 230 1  |-  ( x  =  y  ->  ( ph  ->  A. x ( x  =  y  ->  ph )
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 186   A.wal 1405
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654
This theorem depends on definitions:  df-bi 187
This theorem is referenced by:  ax12wlem  1854
  Copyright terms: Public domain W3C validator