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) mpgbi
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
mpgbi.1 |- ( A. x ph <-> ps )
mpgbi.2 |- ph
Assertion
mpgbi |- ps
Proof
Step
Hyp
Ref
Expression
1
mpgbi.1 |- ( A. x ph <-> ps )
2
mpgbi.2 |- ph
3
2
ax-gen |- A. x ph
4
3 1
mpbi |- ps