Theorem albidv 1679

Description: Formula-building rule for universal quantifier (deduction rule). (Contributed by NM, 26-May-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-5 1670	. 2 |- ( ph -> A. x ph )
2		albidv.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	albidh 1642	1 |- ( ph -> ( A. x ps <-> A. x ch ) )

Syntax hints:   -> wi 4   <-> wb 184   A.wal 1367

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670

This theorem depends on definitions:  df-bi 185

This theorem is referenced by:  2albidv  1681  ax12wdemo  1769  ax12vALT  2131  sbcom2OLD  2152  axc11n-16  2239  eujust  2255  eujustALT  2256  euf  2263  eufOLD  2264  mo2  2265  moOLD  2305  axext3  2425  bm1.1  2427  bm1.1OLD  2428  eqeq1  2449  nfceqdf  2584  ralbidv2  2756  ralxpxfr2d  3103  alexeqg  3107  alexeq  3108  pm13.183  3119  eqeu  3149  mo2icl  3157  euind  3165  reuind  3181  cdeqal  3194  sbcal  3257  sbcalgOLD  3258  sbcabel  3294  csbiebg  3330  ssconb  3508  reldisj  3741  sbcssg  3809  elint  4153  axrep1  4423  axrep2  4424  axrep3  4425  axrep4  4426  zfrepclf  4428  axsep2  4433  zfauscl  4434  bm1.3ii  4435  eusv1  4505  euotd  4611  freq1  4709  frsn  4928  iota5  5420  sbcfung  5460  funimass4  5761  dffo3  5877  eufnfv  5970  dff13  5990  tfisi  6488  dfom2  6497  elom  6498  seqomlem2  6925  pssnn  7550  findcard  7570  findcard2  7571  findcard3  7574  fiint  7607  inf0  7846  axinf2  7865  tz9.1  7968  karden  8121  aceq0  8307  dfac5  8317  zfac  8648  brdom3  8714  axpowndlem3  8783  axpowndlem3OLD  8784  zfcndrep  8800  zfcndac  8805  elgch  8808  engch  8814  axgroth3  9017  axgroth4  9018  elnp  9175  elnpi  9176  infm3  10308  fz1sbc  11555  uzrdgfni  11800  vdwmc2  14059  ramtlecl  14080  ramval  14088  ramub  14093  rami  14095  ramcl  14109  mreexexd  14605  mplsubglem  17529  mpllsslem  17530  mplsubglemOLD  17531  mpllsslemOLD  17532  istopg  18527  1stccn  19086  iskgen3  19141  fbfinnfr  19433  cnextfun  19655  metcld  20835  metcld2  20836  cusgrauvtxb  23423  isass  23822  chlimi  24656  nmcexi  25449  disjrdx  25952  funcnvmpt  26006  relexpindlem  27360  dfon2lem6  27620  dfon2lem7  27621  dfon2lem8  27622  dfon2  27624  sscoid  27963  wl-mo2t  28419  trer  28534  pm14.122b  29700  iotavalb  29707  trsbc  31270  bj-axext3  32312  bj-axrep1  32332  bj-axrep2  32333  bj-axrep3  32334  bj-axrep4  32335  bj-sbceqgALT  32427  bj-axsep2  32451  cdlemefrs29bpre0  34063