Theorem albidv 1656

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

Syntax hints:   -> wi 3   <-> wb 163  A.wal 1296

This theorem is referenced by:  2albidv 1658  sbcom2 1724  eujust 1773  eujustALT 1774  euf 1777  mo 1787  axext3 1867  axext3OLD 1868  bm1.1 1870  eqeq1 1890  hblemOLD 1994  ralbidv2 2125  alexeq 2390  abidhb 2423  mo2icl 2434  moi 2436  euind 2439  reuind 2450  sbc6gOLD 2473  sbcalg 2500  hbsbc1gdOLD 2516  hbsbcgdOLD 2518  sbcralt 2527  sbcralgf 2529  sbcabel 2535  sbcel12gOLD 2553  sbceqdigOLD 2555  csbiegft 2573  ssconb 2738  reldisj 2916  reldisjOLD 2917  elint 3220  elintiOLD 3224  axrep1 3429  axrep2 3430  axrep3 3431  zfrepclf 3434  axsep2 3439  zfauscl 3440  bm1.3ii 3441  elOLD 3486  dtru 3498  freq1 3632  eualeq 3823  eualeqhb 3824  euexeqOLD 3826  euexaleq 3827  onminex 3888  dfom2 3951  elom 3952  elomg 3953  funimass4 4722  eufnfv 4771  dffo3 4792  dff13 4850  ac6sfi 5509  pssnn 5628  unifi 5648  fiint 5650  abfii4 5654  fodomfi 5656  ordtypelem5 5688  ordtypelem6 5689  inf0 5712  axinf2 5730  tz9.1 5753  trsbc 5843  karden 5856  aceq0 5892  aceq5 5902  zfac 5907  brdom3 5963  axpowndlem3 6103  zfcndrep 6118  zfcndac 6123  elnp 6244  prlem934 6291  suplem2pr 6314  supexpr 6315  suppsr 6374  supsrlem6 6382  supre 6412  infm3 7263  infmsup 7277  dfuzi 7414  nnwof 7628  fz1sbc 7696  istopg 8865  islp2 9023  cncnplem3 9053  metcld 9245  axgroth3 10138  axgroth4 10139  oprabopabf 10157  indexfi 10174  findcard 10178  findcardOLD 10179  fbssint 10279  dirtr 10356  isass 10363  chlimi 10737  bnj898 12815  bnj1338 13063  bnj1510 13170  bnj1511 13171  dfon2lem6 13854  dfon2lem7 13855  dfon2lem8 13856  dfon2 13858  elintabg 14414  invtrgrp 14979  eqeu 15351  trer 15361  finsschain 15373  ordtypelem5OLD 15379  ordtypelem6OLD 15380  neibastop2lem3 15521  neibastop3 15524  limfilcf 15587  fcluscf 15612  fcluscomplem 15620  findcard2 15745  indexfiOLD 15755  lmclim2 15850  ax10-16 16365  pm13.183 16373  pm14.122b 16387  iotavalb 16394  isclat 16888

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321

This theorem depends on definitions:  df-bi 164  df-an 242

Copyright terms: Public domain