New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > 2exbidv | GIF version |
Description: Formula-building rule for 2 existential quantifiers (deduction rule). (Contributed by NM, 1-May-1995.) |
Ref | Expression |
---|---|
2albidv.1 | ⊢ (φ → (ψ ↔ χ)) |
Ref | Expression |
---|---|
2exbidv | ⊢ (φ → (∃x∃yψ ↔ ∃x∃yχ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2albidv.1 | . . 3 ⊢ (φ → (ψ ↔ χ)) | |
2 | 1 | exbidv 1626 | . 2 ⊢ (φ → (∃yψ ↔ ∃yχ)) |
3 | 2 | exbidv 1626 | 1 ⊢ (φ → (∃x∃yψ ↔ ∃x∃yχ)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 176 ∃wex 1541 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1546 ax-5 1557 ax-17 1616 |
This theorem depends on definitions: df-bi 177 df-ex 1542 |
This theorem is referenced by: 3exbidv 1629 4exbidv 1630 cbvex4v 2012 ceqsex3v 2897 ceqsex4v 2898 2reu5 3044 elxpk 4196 cnvkeq 4215 ins2keq 4218 ins3keq 4219 sikeq 4241 opkelopkabg 4245 otkelins2kg 4253 otkelins3kg 4254 opkelcokg 4261 opkelsikg 4264 sikss1c1c 4267 copsexg 4607 elopab 4696 brsi 4761 elxpi 4800 brswap2 4860 brswap 5509 cbvoprab3 5571 ov6g 5600 brsnsi 5773 dmpprod 5840 ovce 6172 ceex 6174 elce 6175 |
Copyright terms: Public domain | W3C validator |