Theorem albidv 1705

Description: Formula-building rule for universal quantifier (deduction rule). (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
albidv.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
albidv	|- ( ph -> ( A. x ps <-> A. x ch ) )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   ch( x)

Proof of Theorem albidv

Step	Hyp	Ref	Expression
1		ax-17 1419	. 2 |- ( ph -> A. x ph )
2		albidv.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	albidh 1369	1 |- ( ph -> ( A. x ps <-> A. x ch ) )

Syntax hints:   -> wi 4   <-> wb 98   A.wal 1241

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-17 1419

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  ax11v  1708  2albidv  1747  sbal1yz  1877  eujust  1902  euf  1905  mo23  1941  axext3  2023  bm1.1  2025  eqeq1  2046  nfceqdf  2177  ralbidv2  2328  alexeq  2670  pm13.183  2681  eqeu  2711  mo2icl  2720  euind  2728  reuind  2744  cdeqal  2753  sbcal  2810  sbcalg  2811  sbcabel  2839  csbiebg  2889  ssconb  3076  reldisj  3271  sbcssg  3330  elint  3621  axsep2  3876  zfauscl  3877  bm1.3ii  3878  euotd  3991  freq1  4081  freq2  4083  eusv1  4184  ontr2exmid  4250  regexmid  4260  tfisi  4310  nnregexmid  4342  iota5  4887  sbcfung  4925  funimass4  5224  dffo3  5314  eufnfv  5389  dff13  5407  ssfiexmid  6336  diffitest  6344  findcard  6345  findcard2  6346  findcard2s  6347  fz1sbc  8958  frecuzrdgfn  9198  bdsep2  10006  bdsepnfALT  10009  bdzfauscl  10010  bdbm1.3ii  10011  bj-2inf  10062  bj-nn0sucALT  10103  strcoll2  10108  strcollnfALT  10111