Theorem biexdv 936

Description: Formula-building rule for existential quantifier (deduction rule).

Hypothesis

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

Assertion

Ref	Expression
biexdv	|- (ph -> (E.xps <-> E.xch))

Distinct variable group(s):   ph,x

Proof of Theorem biexdv

Step	Hyp	Ref	Expression
1		ax-17 925	. 2 |- (ph -> A.xph)
2		bialdv.1	. 2 |- (ph -> (ps <-> ch))
3	1, 2	biexd 783	1 |- (ph -> (E.xps <-> E.xch))

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

This theorem is referenced by:  bi2exdv 938  bi3exdv 939  bieud 1012  axinf 1084  axac 1085  eleq1 1149  eleq2 1150  birexdv2 1222  eqvinc 1407  alexeq 1409  ceqex 1410  sbc5g 1450  sbcex 1465  axrep 1473  axrep2 1474  zfrepclf 1477  eluni 1922  unieq 1927  opabid 2099  cbvopab1 2106  cbvopab1s 2107  cbvopab1v 2108  coeq1 2502  coeq2 2503  opelco 2509  opelcog 2511  dfdmf 2526  eldm 2527  eldmg 2529  dmsnop 2547  dfrnf 2561  elrn 2562  iss 2599  cores 2659  ndmfv 2848  fniunfv 2860  dmfco 2864  fvco 2865  fvelrn 2883  rdglem2 2976  rdglim2 2987  cbvoprab12 3028  elqsi 3228  mapsn 3269  breng 3280  brdomg 3281  domeng 3285  zfregcl 3446  inf0 3457  bnd2 3549  aceq0 3553  aceq3lem 3555  aceq3 3556  aceq5lem4 3561  aceq5 3563  ac7g 3570  ac4c 3572  ac5 3573  kmlem1 3580  kmlem2 3581  kmlem9 3588  kmlem12 3591  kmlem13 3592  cfval 3701  cardcf 3706  cfsuc 3709  axrepndlem1 3738  axunndlem1 3741  zfcndrep 3760  zfcndinf 3764  zfcndac 3765  ltexpi 3823  recmulpq 3864  ltexpq 3874  ltexpq2 3875  halfpq 3876  genpn0 3900  genpnmax 3904  1idpr 3927  ltexprlem3 3938  ltexprlem4 3939  ltexpri 3943  reclem2pr 3951  recexpr 3954  recexsrlem 4006  map2psrpr 4014  suppsr 4016  supsrlem6 4024  supre 4054  axnegex 4078  nnunb 4520  infxpidmlem2 4934

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  ax-17 925

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

metamath.org