Theorem albidv 1316

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

Syntax hints:   -> wi 3   <-> wb 144  A.wal 990

This theorem is referenced by:  2albidv 1318  sbcom2 1373  euf 1423  mo 1432  axext3 1502  bm1.1 1504  eqeq1 1524  hblem 1607  ralbidv2 1711  alexeq 1931  abidhb 1958  mo2icl 1969  moi 1971  sbc6g 2000  sbcalg 2022  hbsbc1gd 2031  hbsbcgd 2032  sbcralt 2040  sbcralgf 2042  sbcabel 2046  sbcel12g 2062  sbceqdig 2063  csbiegft 2081  ssconb 2222  reldisj 2366  elint 2606  elinti 2609  axrep1 2768  axrep2 2769  axrep3 2770  zfrepclf 2773  axsep2 2778  zfauscl 2779  bm1.3ii 2780  el 2822  dtru 2831  freq1 2952  onminex 3164  dfom2 3220  elom 3221  elomg 3222  funimass4 3874  dffo3 3933  dff13 3988  ac6sfi 4591  pssnn 4681  unifi 4701  fiint 4703  abfii4 4707  fodomfi 4709  inf0 4751  axinf2 4769  tz9.1 4792  karden 4872  aceq0 4876  aceq5 4886  zfac 4891  brdom3 4947  axpowndlem3 5105  zfcndrep 5120  zfcndac 5125  elnp 5246  prlem934 5293  suplem2pr 5316  supexpr 5317  suppsr 5376  supsrlem6 5384  supre 5414  infm3 6222  infmsup 6236  dfuzi 6373  nnwof 6586  fz1sbc 6648  istopg 7808  islp2 7957  cncnplem3 7986  metcld 8178  axgroth3 9051  axgroth4 9052  chlimi 9380  isass 10890  eqeu 11394  trer 11409  finsschain 11425  ordtypelem5 11431  ordtypelem6 11432  neibastop2lem3 11582  neibastop3 11585  fbssint 11626  limfilcf 11683  fcluscf 11724  fcluscomplem 11732  dirtr 11753  oprabopabf 11807  findcard 11836  indexf 11847  lmclim2 11915

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-17 1007  ax-4 1009  ax-5o 1011

This theorem depends on definitions:  df-bi 145  df-an 223

Copyright terms: Public domain