| 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 form). (Contributed by NM, 1-May-1995.) |
| Ref | Expression |
|---|---|
| 2albidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
| Ref | Expression |
|---|---|
| 2exbidv | ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 ↔ ∃𝑥∃𝑦𝜒)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 2albidv.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
| 2 | 1 | exbidv 1921 | . 2 ⊢ (𝜑 → (∃𝑦𝜓 ↔ ∃𝑦𝜒)) |
| 3 | 2 | exbidv 1921 | 1 ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 ↔ ∃𝑥∃𝑦𝜒)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∃wex 1779 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 |
| This theorem depends on definitions: df-bi 207 df-ex 1780 |
| This theorem is referenced by: 3exbidv 1925 4exbidv 1926 cbvex4vw 2041 cbvex4v 2420 ceqsex3v 3537 ceqsex4v 3538 2reu5 3764 opabbidv 5209 unopab 5224 copsexgw 5495 copsexg 5496 euotd 5518 elopabw 5531 elxpi 5707 relop 5861 dfres3 6002 xpdifid 6188 oprabv 7493 cbvoprab3 7524 elrnmpores 7571 ov6g 7597 omxpenlem 9113 dcomex 10487 ltresr 11180 hashle2prv 14517 fsumcom2 15810 fprodcom2 16020 ispos 18360 fsumvma 27257 1pthon2v 30172 dfconngr1 30207 isconngr 30208 isconngr1 30209 1conngr 30213 conngrv2edg 30214 fusgr2wsp2nb 30353 isacycgr 35150 satfv1 35368 sat1el2xp 35384 elfuns 35916 cbvoprab1vw 36238 cbvoprab1davw 36272 cbvoprab3davw 36274 bj-cbvex4vv 36806 itg2addnclem3 37680 brxrn2 38376 dvhopellsm 41119 diblsmopel 41173 2sbc5g 44435 fundcmpsurinj 47396 ichexmpl1 47456 ichnreuop 47459 ichreuopeq 47460 elsprel 47462 prprelb 47503 reuopreuprim 47513 |
| Copyright terms: Public domain | W3C validator |