Theorem biex 733

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

Hypothesis

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

Assertion

Ref	Expression
biex	|- (E.xph <-> E.xps)

Proof of Theorem biex

Step	Hyp	Ref	Expression
1		19.18 732	. 2 |- (A.x(ph <-> ps) -> (E.xph <-> E.xps))
2		biex.1	. 2 |- (ph <-> ps)
3	1, 2	mpg 684	1 |- (E.xph <-> E.xps)

Syntax hints:   <-> wb 127  E.wex 678

This theorem is referenced by:  bi2ex 734  bi3ex 735  exancom 736  19.29 752  excom13 776  exrot4 778  eeor 795  eqsex 834  19.12vv 960  19.41vv 964  19.41vvv 965  exdistr 967  exdistr2 969  3exdistr 970  4exdistr 971  eeeanv 981  ee4anv 982  sbel2x 995  sb8eu 1017  eu1 1019  eu2 1023  moanim 1051  euanv 1053  2moswap 1064  2exeu 1066  2eu1 1067  exists1 1072  axun 1081  axpow 1082  axinf 1084  axac 1085  clelab 1187  sbabel 1189  birex2 1227  r2ex 1241  r19.29 1295  r19.41v 1302  r19.43 1304  2reuswap 1341  isset 1351  rexv 1358  gencbvex 1372  vtocl2 1379  vtocl3 1380  cla42gv 1399  ceqsrexv 1413  euxfr 1436  zfrep2 1475  zfrep3 1476  zfrep4 1479  zfaus 1480  nvelv 1483  nss 1550  inex1 1697  abn0 1715  pssnel 1752  pwex 1806  snprc 1838  nssss 1866  zfpair 1891  eqvinop 1901  copsexg 1902  eusn 1913  unpr 1930  uniun 1934  uniin 1935  uni0b 1939  uniex 1947  dfiun2 2014  iinss 2025  iunn0 2029  iunxsn 2034  iunxun 2035  opabid 2099  cbvopab2v 2109  unopab 2121  onminex 2275  elxp2 2443  opelxp 2452  cbvop 2473  opelcog 2511  cnvco 2520  cnvuni 2521  dfdm3 2522  dfrn2 2523  dfrn3 2524  dfdm4 2525  eldm2 2528  dmun 2536  dmin 2537  dmuni 2538  dmopab 2539  dmi 2545  elrn2 2563  rnopab 2566  dmco 2570  dmcosseq 2572  dmres 2584  dfima2 2604  dfima3 2605  elima3 2608  imadmrn 2610  imai 2613  imasn 2616  elimasn 2617  intirr 2628  elxp4 2640  elxp5 2641  rnuni 2646  imaiun 2650  coi1 2665  coass 2667  dmco2 2673  dffun2 2674  dffun5 2677  imadif 2714  funimaexg 2715  fcoi1 2765  fcoi2 2766  f11o 2821  fv2 2828  fvopabn 2873  fvresex 2909  isomin 2937  iinon 2948  tfrlem8 2956  dfoprab2 3021  1st2val 3097  ec2 3203  erdmrn 3213  ecdmn0 3217  snec 3232  domen 3284  mapsnen 3334  xpsnen 3339  xpassen 3344  inf0 3457  inf2 3459  inf4 3473  zfinf 3474  tz9.12lem3 3505  scott0 3542  cp 3547  aceq1 3552  aceq0 3553  aceq2 3554  aceq5lem1 3558  aceq5lem2 3559  aceq5lem3 3560  kmlem3 3582  kmlem14 3593  kmlem15 3594  kmlem16 3595  cflem 3700  cf0 3705  axpowndlem3 3745  zfcndrep 3760  zfcndun 3761  zfcndpow 3762  zfcndinf 3764  zfcndac 3765  prnmadd 3894  genpass 3906  1pr 3911  distrlem1pr 3921  ltexprlem1 3936  ltexprlem4 3939  reclem1pr 3950  reclem2pr 3951  suplem1pr 3955  suppsr3 4018  elreal 4044  nnwof 4609  nnwos 4610  infxpidmlem9 4941  osumlem5 5534

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679

metamath.org