Theorem albid 1104

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 998	. 2 |- (ph -> A.x(ps <-> ch))
4		19.15 997	. 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 954

This theorem is referenced by:  19.23t 1116  dral2 1155  ax11v2 1215  hbsb4t 1249  dvelimdf 1251  sbcom 1258  albidv 1278  sbal2 1358  ax11eq 1363  ax11el 1364  ax11indalem 1368  ax11inda2ALT 1369  ax11inda 1371  eubid 1385  ralbida 1657  raleq1f 1783  hbeqd 1913  hbeld 1914  hbsbc1g 1948  hbsbcg 1951  hbsbc1gd 1983  hbsbcgd 1984  hbcsb1gd 2027  hbcsbgd 2028  hbopd 2497  intab 2560  hbbrd 2659  axrep4 2697  hbimad 3412  hbfvd 3730  hbfvd2 3731  hboprd 3982  axrepndlem1 4944  axrepndlem2 4945  axrepnd 4946  axunnd 4948  axpowndlem2 4950  axpowndlem4 4952  axregndlem2 4955  axinfndlem1 4957  axinfnd 4958  axacndlem4 4962  axacndlem5 4963  axacnd 4964  hbnegd 5363

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

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

Copyright terms: Public domain