![]() |
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 1991 | . 2 ⊢ (𝜑 → (∃𝑦𝜓 ↔ ∃𝑦𝜒)) |
3 | 2 | exbidv 1991 | 1 ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 ↔ ∃𝑥∃𝑦𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∃wex 1845 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1863 ax-4 1878 ax-5 1980 |
This theorem depends on definitions: df-bi 197 df-ex 1846 |
This theorem is referenced by: 3exbidv 1994 4exbidv 1995 cbvex4v 2426 ceqsex3v 3378 ceqsex4v 3379 2reu5 3549 copsexg 5096 euotd 5115 elopab 5125 elxpi 5279 relop 5420 dfres3 5548 xpdifid 5712 oprabv 6860 cbvoprab3 6888 elrnmpt2res 6931 ov6g 6955 omxpenlem 8218 dcomex 9453 ltresr 10145 hashle2prv 13444 fsumcom2 14696 fsumcom2OLD 14697 fprodcom2 14905 fprodcom2OLD 14906 ispos 17140 fsumvma 25129 1pthon2v 27297 dfconngr1 27332 isconngr 27333 isconngr1 27334 1conngr 27338 conngrv2edg 27339 fusgr2wsp2nb 27480 elfuns 32320 bj-cbvex4vv 33041 itg2addnclem3 33768 brxrn2 34452 dvhopellsm 36900 diblsmopel 36954 2sbc5g 39111 elsprel 42227 |
Copyright terms: Public domain | W3C validator |