Theorem albidv 1702

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 1416	. 2 |- (ph -> A.xph)
2		albidv.1	. 2 |- (ph -> (ps <-> ch))
3	1, 2	albidh 1366	1 |- (ph -> (A.xps <-> A.xch))

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

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 1333  ax-gen 1335  ax-17 1416

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  ax11v  1705  2albidv  1744  sbal1yz  1874  eujust  1899  euf  1902  mo23  1938  axext3  2020  bm1.1  2022  eqeq1  2043  nfceqdf  2174  ralbidv2  2322  alexeq  2664  pm13.183  2675  eqeu  2705  mo2icl  2714  euind  2722  reuind  2738  cdeqal  2747  sbcal  2804  sbcalg  2805  sbcabel  2833  csbiebg  2883  ssconb  3070  reldisj  3265  sbcssg  3324  elint  3612  axsep2  3867  zfauscl  3868  bm1.3ii  3869  euotd  3982  eusv1  4150  regexmid  4219  tfisi  4253  nnregexmid  4285  iota5  4830  sbcfung  4868  funimass4  5167  dffo3  5257  eufnfv  5332  dff13  5350  ssfiexmid  6254  fz1sbc  8728  frecuzrdgfn  8879  bdsep2  9341  bdsepnfALT  9344  bdzfauscl  9345  bdbm1.3ii  9346  bj-2inf  9397  bj-nn0sucALT  9438  strcoll2  9443  strcollnfALT  9446