Theorem albii 1035

Description: Inference adding universal quantifier to both sides of an equivalence.

Hypothesis

Ref	Expression
albii.1	|- (ph <-> ps)

Assertion

Ref	Expression
albii	|- (A.xph <-> A.xps)

Proof of Theorem albii

Step	Hyp	Ref	Expression
1		19.15 1033	. 2 |- (A.x(ph <-> ps) -> (A.xph <-> A.xps))
2		albii.1	. 2 |- (ph <-> ps)
3	1, 2	mpg 1022	1 |- (A.xph <-> A.xps)

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

This theorem is referenced by:  2albii 1036  hbex 1042  hbor 1044  hban 1045  hbbi 1046  hb3or 1047  hb3an 1048  hbe1 1052  alex 1070  alinexa 1078  exanali 1079  alexn 1080  19.21-2 1093  19.26-2 1104  19.35 1111  19.30 1121  19.32 1122  19.31 1123  19.43 1124  19.41 1131  alrot4 1133  albi 1143  2albi 1144  exintrbi 1154  aaan 1155  equsal 1188  dvelimfALT 1190  dvelimf 1288  sbcom 1296  sb8e 1300  19.23vv 1332  19.12vv 1340  sbcom2 1373  2sb6 1375  sb6a 1376  2sb6rf 1378  sbex 1387  sbalv 1388  2exsb 1390  dvelimALT 1392  sbal2 1397  a12lem2 1416  a12studyALT 1418  hbeu1 1427  hbeu 1428  sb8eu 1429  eu1 1431  eu2 1435  hbmo1 1445  hbmo 1446  moanim 1466  2mo 1487  2eu3 1491  2eu4 1492  exists1 1498  hbab1 1508  hbab 1509  hbabd 1510  eqcom 1520  hbxfr 1606  hbeq 1608  hbel 1609  abeq2 1611  abeq1 1612  eq2ab 1616  sbabel 1627  hbne 1690  ralbii2 1717  r2al 1722  hbral 1732  hbra1 1733  hbrex 1734  hbre1 1735  r3al 1736  r19.21t 1761  r19.22 1777  r19.23v 1787  r19.26 1796  hbreu1 1814  rabid2 1816  ralcom2 1822  ralv 1866  reu2 1976  reu6 1978  rmo4 1979  reu8 1982  2reuswap 1983  hbsbc1v 1995  sbcralt 2040  sbcralgf 2042  ra5 2050  hbcsb1g 2075  hbcsbg 2077  dfss2 2110  hbss 2114  ss2ab 2168  ss2rab 2175  rabss 2176  hbdif 2213  hbun 2238  ssequn1 2252  unss 2256  hbin 2272  ne0f 2340  eqv 2348  disj 2364  disj3 2367  ssdif0 2380  inssdif0 2386  ssundif 2398  hbpw 2464  pwss 2466  hbpr 2484  ralpr 2486  ralsng 2489  sbcsng 2490  eusn 2507  snss 2525  pwpw0 2533  prsspw 2545  pwsnALT 2566  hbuni 2575  unissb 2595  hbint 2610  elintrab 2612  ssintab 2617  intun 2629  intpr 2630  dfiin2 2656  iunss 2659  ssiun 2660  ssiin 2667  iinss 2668  hbbr 2731  dftr2 2756  dftr5 2757  axrep1 2768  axrep5 2772  axsep 2776  zfnuleu 2781  axnul2 2782  vprc 2787  inex1 2790  axpweq 2817  zfpow 2819  axpow2 2820  axpow3 2821  pwex 2823  ssextss 2839  dtruALT 2848  zfpair2 2856  hbopab 2889  dffr2 2949  dfepfr 2960  hbsuc 3044  sucel 3046  zfun 3090  uniex2 3092  hbxp 3287  weinxp 3319  hbrel 3332  eqrelrel 3341  reliun 3354  relop 3365  hbcnv 3386  dmopab3 3413  dm0rn0 3417  reldm0 3418  hbrn 3438  dmcosseq 3452  hbima 3503  dffr3 3523  cotr 3528  asymref 3531  asymref2 3532  intirr 3533  dffun2 3631  dffun3 3632  dffun4 3633  dffun5 3634  dffun6f 3635  hbfun 3641  dffun7 3644  funopab 3653  funcnv2 3661  funcnv 3662  fun2cnv 3664  fun11 3667  fununi 3668  funcnvuni 3669  hbfn 3690  hbf 3732  hbf1 3770  dff12 3771  hbfo 3778  hbf1o 3795  fv2 3831  tz6.12-2 3850  fopab2 3937  dff13 3988  hbiso 4006  tfrlem2 4213  dfer2 4402  ac6sfi 4591  fiint 4703  abfii2 4705  inf2 4753  axinf2 4769  setind2 4795  ranksn 4835  scottexs 4864  scott0s 4865  kardex 4871  karden 4872  aceq1 4875  aceq4 4880  aceq7 4889  ac7 4894  ac6n 4903  kmlem4 4914  kmlem12 4922  kmlem14 4924  kmlem15 4925  kmlem16 4926  aceqkm 4927  axpowndlem3 5105  zfcndrep 5120  zfcndun 5121  zfcndpow 5122  suppsr3 5378  pre-axsup 5445  infm3 6222  infmsup 6236  nnwos 6587  tgss3 7850  ntreq0 7918  islp2 7957  cncfmet 8116  metcnp4 8181  metcn4 8182  nmobndseqi 8695  spwpr2 8920  axgroth2 9050  axgroth4 9052  grothpw 9054  axgroth5 9055  grothprim 9057  choc0 9566  h1deoi 9748  xfree2 10654  difeqri2 10732  ref3w 10772  cnfilca 11088  usinuniop 11128  dfiin2g 11400  inficlALT 11424  ordtypelem7 11433  alexsublem3 11498  cnconn 11503  neibastop2lem3 11582  neibastop2lem4 11583  neibastop2 11584  neibastop3 11585  fbssint 11626  filssufillem 11655  rnelfmlem 11698  lmclim2 11915  heiborlem16 12026

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

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

Copyright terms: Public domain