Theorem albid 1106

Description: Formula-building rule for universal quantifier (deduction rule).

Hypotheses

Ref	Expression
albid.1	|- (ph -> A.xph)
albid.2	|- (ph -> (ps <-> ch))

Assertion

Ref	Expression
albid	|- (ph -> (A.xps <-> A.xch))

Proof of Theorem albid

Step	Hyp	Ref	Expression
1		albid.1	. . 3 |- (ph -> A.xph)
2		albid.2	. . 3 |- (ph -> (ps <-> ch))
3	1, 2	19.21ai 1000	. 2 |- (ph -> A.x(ps <-> ch))
4		19.15 999	. 2 |- (A.x(ps <-> ch) -> (A.xps <-> A.xch))
5	3, 4	syl 10	1 |- (ph -> (A.xps <-> A.xch))

Syntax hints:   -> wi 3   <-> wb 146  A.wal 956

This theorem is referenced by:  19.23t 1118  dral2 1157  ax11v2 1217  hbsb4t 1251  dvelimdf 1253  sbcom 1260  albidv 1280  sbal2 1360  ax11eq 1365  ax11el 1366  ax11indalem 1370  ax11inda2ALT 1371  ax11inda 1373  eubid 1387  ralbida 1660  raleq1f 1786  hbeqd 1916  hbeld 1917  hbsbc1g 1951  hbsbcg 1954  hbsbc1gd 1987  hbsbcgd 1988  hbcsb1gd 2031  hbcsbgd 2032  hbopd 2502  intab 2565  hbbrd 2665  axrep4 2703  hbimad 3419  hbfvd 3737  hbfvd2 3738  hboprd 3989  axrepndlem1 4963  axrepndlem2 4964  axrepnd 4965  axunnd 4967  axpowndlem2 4969  axpowndlem4 4971  axregndlem2 4974  axinfndlem1 4976  axinfnd 4977  axacndlem4 4981  axacndlem5 4982  axacnd 4983  hbnegd 5382

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-4 975  ax-5o 977

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain