Theorem albidv 1796

Description: Formula-building rule for universal quantifier (deduction form). (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 1506	. 2 |- ( ph -> A. x ph )
2		albidv.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	albidh 1456	1 |- ( ph -> ( A. x ps <-> A. x ch ) )

Syntax hints:   -> wi 4   <-> wb 104   A.wal 1329

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-17 1506

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ax11v  1799  2albidv  1839  sbal1yz  1974  eujust  1999  euf  2002  mo23  2038  axext3  2120  bm1.1  2122  eqeq1  2144  nfceqdf  2278  ralbidv2  2437  alexeq  2806  pm13.183  2817  eqeu  2849  mo2icl  2858  euind  2866  reuind  2884  cdeqal  2893  sbcal  2955  sbcalg  2956  sbcabel  2985  csbiebg  3037  ssconb  3204  reldisj  3409  sbcssg  3467  elint  3772  axsep2  4042  zfauscl  4043  bm1.3ii  4044  exmidel  4123  euotd  4171  freq1  4261  freq2  4263  eusv1  4368  ontr2exmid  4435  regexmid  4445  tfisi  4496  nnregexmid  4529  iota5  5103  sbcfung  5142  funimass4  5465  dffo3  5560  eufnfv  5641  dff13  5662  tfr1onlemsucfn  6230  tfr1onlemsucaccv  6231  tfr1onlembxssdm  6233  tfr1onlembfn  6234  tfrcllemsucfn  6243  tfrcllemsucaccv  6244  tfrcllembxssdm  6246  tfrcllembfn  6247  tfrcl  6254  frecabcl  6289  ssfiexmid  6763  domfiexmid  6765  diffitest  6774  findcard  6775  findcard2  6776  findcard2s  6777  fiintim  6810  fisseneq  6813  isomni  7001  isomnimap  7002  ismkv  7020  ismkvmap  7021  exmidfodomrlemr  7051  exmidfodomrlemrALT  7052  fz1sbc  9869  frecuzrdgtcl  10178  frecuzrdgfunlem  10185  zfz1iso  10577  istopg  12155  bdsep2  13073  bdsepnfALT  13076  bdzfauscl  13077  bdbm1.3ii  13078  bj-2inf  13125  bj-nn0sucALT  13165  strcoll2  13170  strcollnfALT  13173