![]() |
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 1526 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | albidv.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | exbidh 1614 | 1 ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 ∃wex 1492 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-4 1510 ax-17 1526 ax-ial 1534 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: ax11ev 1828 2exbidv 1868 3exbidv 1869 eubidh 2032 eubid 2033 eleq1w 2238 eleq2w 2239 eleq1 2240 eleq2 2241 rexbidv2 2480 ceqsex2 2779 alexeq 2865 ceqex 2866 sbc5 2988 sbcex2 3018 sbcexg 3019 sbcabel 3046 eluni 3814 csbunig 3819 intab 3875 cbvopab1 4078 cbvopab1s 4080 axsep2 4124 zfauscl 4125 bnd2 4175 mss 4228 opeqex 4251 euotd 4256 snnex 4450 uniuni 4453 regexmid 4536 reg2exmid 4537 onintexmid 4574 reg3exmid 4581 nnregexmid 4622 opeliunxp 4683 csbxpg 4709 brcog 4796 elrn2g 4819 dfdmf 4822 csbdmg 4823 eldmg 4824 dfrnf 4870 elrn2 4871 elrnmpt1 4880 brcodir 5018 xp11m 5069 xpimasn 5079 csbrng 5092 elxp4 5118 elxp5 5119 dfco2a 5131 cores 5134 funimaexglem 5301 brprcneu 5510 ssimaexg 5580 dmfco 5586 fndmdif 5623 fmptco 5684 fliftf 5802 acexmidlem2 5874 acexmidlemv 5875 cbvoprab1 5949 cbvoprab2 5950 oprssdmm 6174 dmtpos 6259 tfrlemi1 6335 tfr1onlemaccex 6351 tfrcllemaccex 6364 ecdmn0m 6579 ereldm 6580 elqsn0m 6605 mapsn 6692 bren 6749 brdomg 6750 domeng 6754 ac6sfi 6900 ordiso 7037 ctssdclemr 7113 enumct 7116 ctssexmid 7150 exmidfodomrlemr 7203 exmidfodomrlemrALT 7204 acfun 7208 ccfunen 7265 cc1 7266 cc2lem 7267 cc2 7268 cc3 7269 recexnq 7391 prarloc 7504 genpdflem 7508 genpassl 7525 genpassu 7526 ltexprlemell 7599 ltexprlemelu 7600 ltexprlemm 7601 recexprlemell 7623 recexprlemelu 7624 cnm 7833 sup3exmid 8916 seq3f1olemp 10504 zfz1isolem1 10822 zfz1iso 10823 sumeq1 11365 sumeq2 11369 summodc 11393 fsum3 11397 fsum2dlemstep 11444 ntrivcvgap0 11559 prodeq1f 11562 prodeq2w 11566 prodeq2 11567 prodmodc 11588 zproddc 11589 fprodseq 11593 fprodntrivap 11594 fprod2dlemstep 11632 ctinf 12433 ctiunct 12443 ssomct 12448 ptex 12718 islssm 13450 bdsep2 14723 bdzfauscl 14727 strcoll2 14820 sscoll2 14825 subctctexmid 14835 nninfall 14843 |
Copyright terms: Public domain | W3C validator |