Theorem albidv 1625

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.xps <-> A.xch))

Distinct variable group:   ph,x

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

Proof of Theorem albidv

Step	Hyp	Ref	Expression
1		ax-17 1616	. 2 |- (ph -> A.xph)
2		albidv.1	. 2 |- (ph -> (ps <-> ch))
3	1, 2	albidh 1590	1 |- (ph -> (A.xps <-> A.xch))

Syntax hints:   -> wi 4   <-> wb 176  A.wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  2albidv  1627  ax11wdemo  1723  ax11vALT  2097  sbcom2  2114  ax10-16  2190  eujust  2206  eujustALT  2207  euf  2210  mo  2226  axext3  2336  bm1.1  2338  eqeq1  2359  nfceqdf  2489  ralbidv2  2637  alexeq  2969  pm13.183  2980  eqeu  3008  mo2icl  3016  euind  3024  reuind  3040  sbcal  3094  sbcalg  3095  sbcabel  3124  csbiebg  3176  ssconb  3400  reldisj  3595  sbcss  3661  elint  3933  iota5  4360  nnadjoin  4521  sfintfin  4533  tfinnn  4535  spfinsfincl  4540  spfininduct  4541  ssrel  4845  funimass4  5369  dffo3  5423  dff13  5472  fnfullfunlem1  5857  frd  5923