Theorem albidv 1273

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

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

This theorem is referenced by:  2albidv 1275  sbcom2 1329  euf 1377  mo 1386  zfext2 1454  bm1.1 1455  eqeq1 1473  hblem 1556  ralbidv2 1657  alexeq 1876  abidhb 1903  mo2icl 1914  moi 1915  sbc6g 1945  sbcalg 1964  hbsbc1gd 1973  hbsbcgd 1974  sbcralt 1980  sbcralgf 1982  sbcabel 1986  sbcel12g 2001  sbceqdig 2002  csbiegft 2019  ssconb 2160  reldisj 2303  elint 2529  elinti 2532  axrep1 2684  axrep2 2685  axrep3 2686  zfrepclf 2689  axsep2 2694  zfauscl 2695  bm1.3ii 2696  dtruALT 2738  freq1 2912  onminex 3010  dfom2 3123  elom 3124  elomg 3125  funimass4 3748  dffo3 3804  f1fv 3859  pssnn 4513  unifi 4532  fiint 4534  abfii4 4538  fodomfi 4540  inf0 4578  axinf2 4596  tz9.1 4618  karden 4698  aceq0 4702  aceq5 4712  axac 4717  brdom3 4773  axpowndlem3 4923  zfcndrep 4938  zfcndac 4943  elnp 5064  prlem934 5111  suplem2pr 5134  supexpr 5135  suppsr 5194  supsrlem6 5202  supre 5232  infm3 6001  infmsup 6015  dfuz 6150  nnwof 6391  fz1sbct 6449  istopg 7538  islp2 7688  cncnplem3 7715  metcld 7901  axgroth3 8718  axgroth4 8719  chlim 9025

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972

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

Copyright terms: Public domain