Theorem albid 1459

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 1345	. 2 |- (ph -> A.x(ps <-> ch))
4		albi 1344	. 2 |- (A.x(ps <-> ch) -> (A.xps <-> A.xch))
5	3, 4	syl 12	1 |- (ph -> (A.xps <-> A.xch))

Syntax hints:   -> wi 3   <-> wb 163  A.wal 1296

This theorem is referenced by:  19.23t 1474  dral2 1516  ax11v2 1585  hbsb4tOLD 1622  dvelimdf 1624  sbcom 1632  albidv 1656  sbal2 1749  ax11eq 1754  ax11el 1755  ax11indalem 1759  ax11inda2ALT 1760  ax11inda 1762  eubid 1778  ralbida 2117  raleqf 2263  hbeqd 2424  hbeld 2425  hbsbc1g 2461  hbsbcg 2466  hbsbc1gd 2515  hbsbc1gdOLD 2516  hbsbcgd 2517  hbsbcgdOLD 2518  hbcsb1gd 2570  hbcsbgd 2571  hbopd 3169  intab 3247  hbbrdOLD 3383  axrep4 3432  eualeqhb 3824  euexeqOLD 3826  euexaleq 3827  hbimad 4275  hbfvd 4687  hbfvd2 4688  hboprdOLD 4906  axrepndlem1 6096  axrepndlem2 6097  axrepnd 6098  axunnd 6100  axpowndlem2 6102  axpowndlem4 6104  axregndlem2 6107  axinfndlem1 6109  axinfnd 6110  axacndlem4 6114  axacndlem5 6115  axacnd 6116  hbnegdOLD 6519  bnj1512 13172  bnj1513 13173  hbprod 14660  btmp 15252  2albi 16330

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-4 1319  ax-5o 1321

This theorem depends on definitions:  df-bi 164  df-an 242

Copyright terms: Public domain