![]() |
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 1925 | . 2 ⊢ (𝜑 → (∃𝑦𝜓 ↔ ∃𝑦𝜒)) |
3 | 2 | exbidv 1925 | 1 ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 ↔ ∃𝑥∃𝑦𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∃wex 1782 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 |
This theorem depends on definitions: df-bi 206 df-ex 1783 |
This theorem is referenced by: 3exbidv 1929 4exbidv 1930 cbvex4vw 2046 cbvex4v 2415 ceqsex3v 3530 ceqsex4v 3531 2reu5 3752 opabbidv 5210 unopab 5226 copsexgw 5486 copsexg 5487 euotd 5509 elopabw 5522 elxpi 5694 relop 5845 dfres3 5981 xpdifid 6159 oprabv 7456 cbvoprab3 7487 elrnmpores 7533 ov6g 7558 omxpenlem 9061 dcomex 10429 ltresr 11122 hashle2prv 14426 fsumcom2 15707 fprodcom2 15915 ispos 18254 fsumvma 26683 1pthon2v 29373 dfconngr1 29408 isconngr 29409 isconngr1 29410 1conngr 29414 conngrv2edg 29415 fusgr2wsp2nb 29554 isacycgr 34067 satfv1 34285 sat1el2xp 34301 elfuns 34818 bj-cbvex4vv 35588 itg2addnclem3 36446 brxrn2 37151 dvhopellsm 39894 diblsmopel 39948 2sbc5g 43046 fundcmpsurinj 45950 ichexmpl1 46010 ichnreuop 46013 ichreuopeq 46014 elsprel 46016 prprelb 46057 reuopreuprim 46067 |
Copyright terms: Public domain | W3C validator |