![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > exbidv | GIF version |
Description: Formula-building rule for existential quantifier (deduction rule). (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
albidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
exbidv | ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-17 1460 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | albidv.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | exbidh 1546 | 1 ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 103 ∃wex 1422 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1377 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-4 1441 ax-17 1460 ax-ial 1468 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: ax11ev 1750 2exbidv 1790 3exbidv 1791 eubidh 1948 eubid 1949 eleq1 2142 eleq2 2143 rexbidv2 2372 ceqsex2 2640 alexeq 2722 ceqex 2723 sbc5 2839 sbcex2 2868 sbcexg 2869 sbcabel 2896 eluni 3612 csbunig 3617 intab 3673 cbvopab1 3859 cbvopab1s 3861 axsep2 3905 zfauscl 3906 bnd2 3955 mss 3989 opeqex 4012 euotd 4017 snnex 4207 uniuni 4209 regexmid 4286 reg2exmid 4287 onintexmid 4323 reg3exmid 4330 nnregexmid 4368 opeliunxp 4421 csbxpg 4447 brcog 4530 elrn2g 4553 dfdmf 4556 csbdmg 4557 eldmg 4558 dfrnf 4603 elrn2 4604 elrnmpt1 4613 brcodir 4742 xp11m 4789 xpimasn 4799 csbrng 4812 elxp4 4838 elxp5 4839 dfco2a 4851 cores 4854 funimaexglem 5013 brprcneu 5202 ssimaexg 5267 dmfco 5273 fndmdif 5304 fmptco 5362 fliftf 5470 acexmidlem2 5540 acexmidlemv 5541 cbvoprab1 5607 cbvoprab2 5608 dmtpos 5905 tfrlemi1 5981 tfr1onlemaccex 5997 tfrcllemaccex 6010 ecdmn0m 6214 ereldm 6215 elqsn0m 6240 bren 6294 brdomg 6295 domeng 6299 ac6sfi 6431 ordiso 6506 recexnq 6642 prarloc 6755 genpdflem 6759 genpassl 6776 genpassu 6777 ltexprlemell 6850 ltexprlemelu 6851 ltexprlemm 6852 recexprlemell 6874 recexprlemelu 6875 sumeq1 10330 sumeq2d 10334 sumeq2 10335 bdsep2 10835 bdzfauscl 10839 strcoll2 10936 |
Copyright terms: Public domain | W3C validator |