Theorem albidv 1280

Description: Formula-building rule for universal quantifier (deduction rule).

Hypothesis

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

Assertion

Ref	Expression
albidv	|- (ph -> (A.xps <-> A.xch))

Distinct variable group:   ph,x

Proof of Theorem albidv

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

Syntax hints:   -> wi 3   <-> wb 146  A.wal 956

This theorem is referenced by:  2albidv 1282  sbcom2 1336  euf 1386  mo 1395  zfext2 1464  bm1.1 1465  eqeq1 1484  hblem 1567  ralbidv2 1668  alexeq 1888  abidhb 1915  mo2icl 1926  moi 1928  sbc6g 1958  sbcalg 1977  hbsbc1gd 1986  hbsbcgd 1987  sbcralt 1993  sbcralgf 1995  sbcabel 1999  sbcel12g 2014  sbceqdig 2015  csbiegft 2032  ssconb 2173  reldisj 2317  elint 2543  elinti 2546  axrep1 2699  axrep2 2700  axrep3 2701  zfrepclf 2704  axsep2 2709  zfauscl 2710  bm1.3ii 2711  dtruALT 2754  freq1 2928  onminex 3026  dfom2 3139  elom 3140  elomg 3141  funimass4 3769  dffo3 3825  f1fv 3880  pssnn 4544  unifiOLD 4570  fiint 4572  fiintOLD 4573  fodomfi 4575  fodomfiOLD 4576  inf0 4615  axinf2 4633  tz9.1 4656  karden 4736  aceq0 4740  aceq5 4750  axac 4755  brdom3 4811  axpowndlem3 4963  zfcndrep 4978  zfcndac 4983  elnp 5104  prlem934 5151  suplem2pr 5174  supexpr 5175  suppsr 5234  supsrlem6 5242  supre 5272  infm3 6056  infmsup 6070  dfuz 6204  nnwof 6460  fz1sbct 6518  istopg 7598  islp2 7744  cncnplem3 7773  metcld 7964  axgroth3 8774  axgroth4 8775  chlim 9099

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain