Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > exbidv | GIF version |
Description: Formula-building rule for existential quantifier (deduction form). (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
albidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
exbidv | ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-17 1506 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | albidv.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | exbidh 1593 | 1 ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 ∃wex 1468 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1423 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-4 1487 ax-17 1506 ax-ial 1514 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: ax11ev 1800 2exbidv 1840 3exbidv 1841 eubidh 2005 eubid 2006 eleq1w 2200 eleq2w 2201 eleq1 2202 eleq2 2203 rexbidv2 2440 ceqsex2 2726 alexeq 2811 ceqex 2812 sbc5 2932 sbcex2 2962 sbcexg 2963 sbcabel 2990 eluni 3739 csbunig 3744 intab 3800 cbvopab1 4001 cbvopab1s 4003 axsep2 4047 zfauscl 4048 bnd2 4097 mss 4148 opeqex 4171 euotd 4176 snnex 4369 uniuni 4372 regexmid 4450 reg2exmid 4451 onintexmid 4487 reg3exmid 4494 nnregexmid 4534 opeliunxp 4594 csbxpg 4620 brcog 4706 elrn2g 4729 dfdmf 4732 csbdmg 4733 eldmg 4734 dfrnf 4780 elrn2 4781 elrnmpt1 4790 brcodir 4926 xp11m 4977 xpimasn 4987 csbrng 5000 elxp4 5026 elxp5 5027 dfco2a 5039 cores 5042 funimaexglem 5206 brprcneu 5414 ssimaexg 5483 dmfco 5489 fndmdif 5525 fmptco 5586 fliftf 5700 acexmidlem2 5771 acexmidlemv 5772 cbvoprab1 5843 cbvoprab2 5844 oprssdmm 6069 dmtpos 6153 tfrlemi1 6229 tfr1onlemaccex 6245 tfrcllemaccex 6258 ecdmn0m 6471 ereldm 6472 elqsn0m 6497 mapsn 6584 bren 6641 brdomg 6642 domeng 6646 ac6sfi 6792 ordiso 6921 ctssdclemr 6997 enumct 7000 ctssexmid 7024 exmidfodomrlemr 7058 exmidfodomrlemrALT 7059 acfun 7063 ccfunen 7079 recexnq 7198 prarloc 7311 genpdflem 7315 genpassl 7332 genpassu 7333 ltexprlemell 7406 ltexprlemelu 7407 ltexprlemm 7408 recexprlemell 7430 recexprlemelu 7431 cnm 7640 sup3exmid 8715 seq3f1olemp 10275 zfz1isolem1 10583 zfz1iso 10584 sumeq1 11124 sumeq2 11128 summodc 11152 fsum3 11156 fsum2dlemstep 11203 ntrivcvgap0 11318 prodeq1f 11321 prodeq2w 11325 prodeq2 11326 prodmodc 11347 ctinf 11943 ctiunct 11953 bdsep2 13084 bdzfauscl 13088 strcoll2 13181 subctctexmid 13196 nninfall 13204 |
Copyright terms: Public domain | W3C validator |