![]() |
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 1474 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | albidv.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | exbidh 1561 | 1 ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 ∃wex 1436 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1391 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-4 1455 ax-17 1474 ax-ial 1482 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: ax11ev 1767 2exbidv 1807 3exbidv 1808 eubidh 1966 eubid 1967 eleq1w 2160 eleq2w 2161 eleq1 2162 eleq2 2163 rexbidv2 2399 ceqsex2 2681 alexeq 2765 ceqex 2766 sbc5 2885 sbcex2 2914 sbcexg 2915 sbcabel 2942 eluni 3686 csbunig 3691 intab 3747 cbvopab1 3941 cbvopab1s 3943 axsep2 3987 zfauscl 3988 bnd2 4037 mss 4086 opeqex 4109 euotd 4114 snnex 4307 uniuni 4310 regexmid 4388 reg2exmid 4389 onintexmid 4425 reg3exmid 4432 nnregexmid 4472 opeliunxp 4532 csbxpg 4558 brcog 4644 elrn2g 4667 dfdmf 4670 csbdmg 4671 eldmg 4672 dfrnf 4718 elrn2 4719 elrnmpt1 4728 brcodir 4862 xp11m 4913 xpimasn 4923 csbrng 4936 elxp4 4962 elxp5 4963 dfco2a 4975 cores 4978 funimaexglem 5142 brprcneu 5346 ssimaexg 5415 dmfco 5421 fndmdif 5457 fmptco 5518 fliftf 5632 acexmidlem2 5703 acexmidlemv 5704 cbvoprab1 5775 cbvoprab2 5776 dmtpos 6083 tfrlemi1 6159 tfr1onlemaccex 6175 tfrcllemaccex 6188 ecdmn0m 6401 ereldm 6402 elqsn0m 6427 mapsn 6514 bren 6571 brdomg 6572 domeng 6576 ac6sfi 6721 ordiso 6836 ctssdclemr 6911 enumct 6914 ctssexmid 6936 exmidfodomrlemr 6967 exmidfodomrlemrALT 6968 recexnq 7099 prarloc 7212 genpdflem 7216 genpassl 7233 genpassu 7234 ltexprlemell 7307 ltexprlemelu 7308 ltexprlemm 7309 recexprlemell 7331 recexprlemelu 7332 sup3exmid 8573 seq3f1olemp 10116 zfz1isolem1 10424 zfz1iso 10425 sumeq1 10963 sumeq2 10967 summodc 10991 fsum3 10995 fsum2dlemstep 11042 ctinf 11735 bdsep2 12665 bdzfauscl 12669 strcoll2 12766 nninfall 12788 |
Copyright terms: Public domain | W3C validator |