Theorem albidv 1278

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

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

This theorem is referenced by:  2albidv 1280  sbcom2 1334  euf 1384  mo 1393  zfext2 1461  bm1.1 1462  eqeq1 1481  hblem 1564  ralbidv2 1665  alexeq 1885  abidhb 1912  mo2icl 1923  moi 1925  sbc6g 1955  sbcalg 1974  hbsbc1gd 1983  hbsbcgd 1984  sbcralt 1990  sbcralgf 1992  sbcabel 1996  sbcel12g 2011  sbceqdig 2012  csbiegft 2029  ssconb 2170  reldisj 2313  elint 2539  elinti 2542  axrep1 2694  axrep2 2695  axrep3 2696  zfrepclf 2699  axsep2 2704  zfauscl 2705  bm1.3ii 2706  dtruALT 2748  freq1 2922  onminex 3020  dfom2 3133  elom 3134  elomg 3135  funimass4 3763  dffo3 3819  f1fv 3874  pssnn 4534  unifiOLD 4557  fiint 4559  fiintOLD 4560  abfii4OLD 4564  fodomfiOLD 4566  inf0 4606  axinf2 4624  tz9.1 4646  karden 4726  aceq0 4730  aceq5 4740  axac 4745  brdom3 4801  axpowndlem3 4951  zfcndrep 4966  zfcndac 4971  elnp 5092  prlem934 5139  suplem2pr 5162  supexpr 5163  suppsr 5222  supsrlem6 5230  supre 5260  infm3 6054  infmsup 6068  dfuz 6202  nnwof 6459  fz1sbct 6517  istopg 7596  islp2 7747  cncnplem3 7776  metcld 7967  axgroth3 8779  axgroth4 8780  chlim 9104

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

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

Copyright terms: Public domain