Theorem albidv 1276

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 969	. 2 |- (ph -> A.xph)
2		albidv.1	. 2 |- (ph -> (ps <-> ch))
3	1, 2	albid 1102	1 |- (ph -> (A.xps <-> A.xch))

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

This theorem is referenced by:  2albidv 1278  sbcom2 1332  euf 1382  mo 1391  zfext2 1459  bm1.1 1460  eqeq1 1478  hblem 1561  ralbidv2 1662  alexeq 1881  abidhb 1908  mo2icl 1919  moi 1921  sbc6g 1951  sbcalg 1970  hbsbc1gd 1979  hbsbcgd 1980  sbcralt 1986  sbcralgf 1988  sbcabel 1992  sbcel12g 2007  sbceqdig 2008  csbiegft 2025  ssconb 2166  reldisj 2309  elint 2534  elinti 2537  axrep1 2689  axrep2 2690  axrep3 2691  zfrepclf 2694  axsep2 2699  zfauscl 2700  bm1.3ii 2701  dtruALT 2743  freq1 2917  onminex 3015  dfom2 3128  elom 3129  elomg 3130  funimass4 3754  dffo3 3810  f1fv 3865  pssnn 4519  unifi 4538  fiint 4540  abfii4 4544  fodomfi 4546  inf0 4586  axinf2 4604  tz9.1 4626  karden 4706  aceq0 4710  aceq5 4720  axac 4725  brdom3 4781  axpowndlem3 4931  zfcndrep 4946  zfcndac 4951  elnp 5072  prlem934 5119  suplem2pr 5142  supexpr 5143  suppsr 5202  supsrlem6 5210  supre 5240  infm3 6009  infmsup 6023  dfuz 6158  nnwof 6399  fz1sbct 6457  istopg 7546  islp2 7697  cncnplem3 7726  metcld 7917  axgroth3 8718  axgroth4 8719  chlim 9043

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973

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

Copyright terms: Public domain