Theorem albidv 1925

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

Syntax hints:   -> wi 3   <-> wb 219  A.wal 1584

This theorem is referenced by:  2albidv 1927  sbcom2 1990  eujust 2039  eujustALT 2040  euf 2043  mo 2053  axext3 2125  bm1.1 2127  eqeq1 2147  ralbidv2 2375  alexeq 2630  abidhb 2664  mo2icl 2679  moi 2681  euind 2685  reuind 2696  sbcalg 2737  sbcralt 2759  sbcralgf 2761  sbcabel 2766  csbiegft 2804  csbiebg 2806  ssconb 2957  reldisj 3121  elint 3406  axrep1 3597  axrep2 3598  axrep3 3599  zfrepclf 3602  axsep2 3607  zfauscl 3608  bm1.3ii 3609  dtru 3662  freq1 3787  eusv1 3960  eusvhb 3961  eusv2OLD 3963  eusv2 3964  onminex 4031  dfom2 4087  elom 4088  elomg 4089  funimass4 4808  eufnfv 4857  dffo3 4882  dff13 4945  oprabopabf 5170  ac6sfi 5675  pssnn 5834  findcard 5843  findcard2 5844  unifi 5870  fiint 5872  abfii4 5876  indexfi 5878  fodomfi 5880  ordtypelem5 5919  ordtypelem6 5920  inf0 5944  axinf2 5963  tz9.1 5989  trsbc 6073  karden 6095  aceq0 6184  aceq5 6194  zfac 6315  brdom3 6377  axpowndlem3 6469  zfcndrep 6484  zfcndac 6489  elnp 6610  prlem934 6657  suplem2pr 6680  supexpr 6681  suppsr 6740  supsrlem6 6748  supre 6778  infm3 7603  infmsup 7617  dfuzi 7757  nnwof 7975  fz1sbc 8067  isclat 9671  istopg 9700  islp2 9889  cncnplem3 9919  metcld 10111  axgroth3 11009  axgroth4 11010  fbssint 11117  dirtr 11194  isass 11201  chlimi 11571  bnj898 13586  bnj1338 13834  bnj1510 13941  bnj1511 13942  dfon2lem6 14488  dfon2lem7 14489  dfon2lem8 14490  dfon2 14492  alexeqd 15002  elintabg 15126  invtrgrp 15757  eqeu 16175  trer 16185  finsschain 16197  ordtypelem5OLD 16203  ordtypelem6OLD 16204  neibastop2lem3 16345  neibastop3 16348  limfilcf 16411  fcluscf 16436  fcluscomplem 16444  findcard2OLD 16569  indexfiOLD 16579  lmclim2 16674  ax10-16 17189  pm13.183 17197  pm14.122b 17211  iotavalb 17218  cdlemefrs29bpre0 18770

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1593  ax-17 1605  ax-4 1608  ax-5o 1610

This theorem depends on definitions:  df-bi 220

Copyright terms: Public domain