Theorem biald 782

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

Hypotheses

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

Assertion

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

Proof of Theorem biald

Step	Hyp	Ref	Expression
1		biald.1	. . 3 |- (ph -> A.xph)
2		biald.2	. . 3 |- (ph -> (ps <-> ch))
3	1, 2	19.21ai 740	. 2 |- (ph -> A.x(ps <-> ch))
4		19.15 694	. 2 |- (A.x(ps <-> ch) -> (A.xps <-> A.xch))
5	3, 4	syl 12	1 |- (ph -> (A.xps <-> A.xch))

Syntax hints:   -> wi 2   <-> wb 127  A.wal 672

This theorem is referenced by:  hbsb4t 906  ddelimdf 909  sbcom 916  bialdv 935  sbal2 1005  bieud 1012  biralda 1213  rgen2 1248  ralcom2 1314  raleqf 1321  hbsbcg 1445  zfrep2 1475  axrepndlem1 3738  axrepndlem2 3739  axrepnd 3740  axunnd 3742  axpowndlem2 3744  axpowndlem4 3746  axpownd 3747  axregndlem2 3749  axinfndlem1 3751  axinfnd 3752  axacndlem4 3756  axacndlem5 3757  axacnd 3758

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org