Theorem albid 1103

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

This theorem is referenced by:  19.23t 1115  dral2 1154  ax11v2 1214  hbsb4t 1248  dvelimdf 1250  sbcom 1257  albidv 1277  sbal2 1357  ax11eq 1362  ax11el 1363  ax11indalem 1367  ax11inda2ALT 1368  ax11inda 1370  eubid 1384  ralbida 1655  raleq1f 1781  hbeqd 1910  hbeld 1911  hbsbc1g 1945  hbsbcg 1948  hbsbc1gd 1980  hbsbcgd 1981  hbcsb1gd 2024  hbcsbgd 2025  hbopd 2494  intab 2556  hbbrd 2655  axrep4 2693  hbimad 3408  hbfvd 3725  hbfvd2 3726  hboprd 3977  axrepndlem1 4927  axrepndlem2 4928  axrepnd 4929  axunnd 4931  axpowndlem2 4933  axpowndlem4 4935  axregndlem2 4938  axinfndlem1 4940  axinfnd 4941  axacndlem4 4945  axacndlem5 4946  axacnd 4947  hbnegd 5346

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-4 972  ax-5o 974

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

Copyright terms: Public domain