This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY Predicate calculus with equality: Tarski's system S2 (1 rule, 6 schemes) Rule scheme ax-gen (Generalization) mpgbir
Description: Modus ponens on biconditional combined with generalization.
(Contributed by NM , 24-May-1994) (Proof shortened by Stefan Allan , 28-Oct-2008)
Ref
Expression
Hypotheses
mpgbir.1 |- ( ph <-> A. x ps )
mpgbir.2 |- ps
Assertion
mpgbir |- ph
Proof
Step
Hyp
Ref
Expression
1
mpgbir.1 |- ( ph <-> A. x ps )
2
mpgbir.2 |- ps
3
2
ax-gen |- A. x ps
4
3 1
mpbir |- ph