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 1519 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | albidv.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | exbidh 1607 | 1 ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 ∃wex 1485 |
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 1440 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-4 1503 ax-17 1519 ax-ial 1527 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: ax11ev 1821 2exbidv 1861 3exbidv 1862 eubidh 2025 eubid 2026 eleq1w 2231 eleq2w 2232 eleq1 2233 eleq2 2234 rexbidv2 2473 ceqsex2 2770 alexeq 2856 ceqex 2857 sbc5 2978 sbcex2 3008 sbcexg 3009 sbcabel 3036 eluni 3797 csbunig 3802 intab 3858 cbvopab1 4060 cbvopab1s 4062 axsep2 4106 zfauscl 4107 bnd2 4157 mss 4209 opeqex 4232 euotd 4237 snnex 4431 uniuni 4434 regexmid 4517 reg2exmid 4518 onintexmid 4555 reg3exmid 4562 nnregexmid 4603 opeliunxp 4664 csbxpg 4690 brcog 4776 elrn2g 4799 dfdmf 4802 csbdmg 4803 eldmg 4804 dfrnf 4850 elrn2 4851 elrnmpt1 4860 brcodir 4996 xp11m 5047 xpimasn 5057 csbrng 5070 elxp4 5096 elxp5 5097 dfco2a 5109 cores 5112 funimaexglem 5279 brprcneu 5487 ssimaexg 5556 dmfco 5562 fndmdif 5598 fmptco 5659 fliftf 5775 acexmidlem2 5847 acexmidlemv 5848 cbvoprab1 5922 cbvoprab2 5923 oprssdmm 6147 dmtpos 6232 tfrlemi1 6308 tfr1onlemaccex 6324 tfrcllemaccex 6337 ecdmn0m 6551 ereldm 6552 elqsn0m 6577 mapsn 6664 bren 6721 brdomg 6722 domeng 6726 ac6sfi 6872 ordiso 7009 ctssdclemr 7085 enumct 7088 ctssexmid 7122 exmidfodomrlemr 7166 exmidfodomrlemrALT 7167 acfun 7171 ccfunen 7213 cc1 7214 cc2lem 7215 cc2 7216 cc3 7217 recexnq 7339 prarloc 7452 genpdflem 7456 genpassl 7473 genpassu 7474 ltexprlemell 7547 ltexprlemelu 7548 ltexprlemm 7549 recexprlemell 7571 recexprlemelu 7572 cnm 7781 sup3exmid 8860 seq3f1olemp 10445 zfz1isolem1 10762 zfz1iso 10763 sumeq1 11305 sumeq2 11309 summodc 11333 fsum3 11337 fsum2dlemstep 11384 ntrivcvgap0 11499 prodeq1f 11502 prodeq2w 11506 prodeq2 11507 prodmodc 11528 zproddc 11529 fprodseq 11533 fprodntrivap 11534 fprod2dlemstep 11572 ctinf 12372 ctiunct 12382 ssomct 12387 bdsep2 13843 bdzfauscl 13847 strcoll2 13940 sscoll2 13945 subctctexmid 13956 nninfall 13964 |
Copyright terms: Public domain | W3C validator |