Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 2exbidv | Structured version Visualization version GIF version |
Description: Formula-building rule for two existential quantifiers (deduction rule). (Contributed by NM, 1-May-1995.) |
Ref | Expression |
---|---|
2albidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
2exbidv | ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 ↔ ∃𝑥∃𝑦𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2albidv.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | exbidv 1837 | . 2 ⊢ (𝜑 → (∃𝑦𝜓 ↔ ∃𝑦𝜒)) |
3 | 2 | exbidv 1837 | 1 ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 ↔ ∃𝑥∃𝑦𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∃wex 1695 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 |
This theorem depends on definitions: df-bi 196 df-ex 1696 |
This theorem is referenced by: 3exbidv 1840 4exbidv 1841 cbvex4v 2277 ceqsex3v 3219 ceqsex4v 3220 2reu5 3383 copsexg 4882 euotd 4900 elopab 4908 elxpi 5054 relop 5194 xpdifid 5481 oprabv 6601 cbvoprab3 6629 elrnmpt2res 6672 ov6g 6696 omxpenlem 7946 dcomex 9152 ltresr 9840 fsumcom2 14347 fsumcom2OLD 14348 fprodcom2 14553 fprodcom2OLD 14554 ispos 16770 fsumvma 24738 dfconngra1 26199 isconngra 26200 isconngra1 26201 1conngra 26203 is2wlkonot 26390 is2spthonot 26391 2wlkonot 26392 2spthonot 26393 el2wlkonot 26396 el2spthonot 26397 el2spthonot0 26398 el2wlkonotot0 26399 2wlkonot3v 26402 2spthonot3v 26403 usg2wotspth 26411 2pthwlkonot 26412 2spotdisj 26588 usg2spot2nb 26592 dfres3 30902 elfuns 31192 bj-cbvex4vv 31930 itg2addnclem3 32633 dvhopellsm 35424 diblsmopel 35478 2sbc5g 37639 1pthon2v-av 41320 dfconngr1 41355 isconngr 41356 isconngr1 41357 1conngr 41361 conngrv2edg 41362 fusgr2wsp2nb 41498 |
Copyright terms: Public domain | W3C validator |