![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3exbii | Structured version Visualization version GIF version |
Description: Inference adding three existential quantifiers to both sides of an equivalence. (Contributed by NM, 2-May-1995.) |
Ref | Expression |
---|---|
3exbii.1 | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
3exbii | ⊢ (∃𝑥∃𝑦∃𝑧𝜑 ↔ ∃𝑥∃𝑦∃𝑧𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3exbii.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
2 | 1 | exbii 1850 | . 2 ⊢ (∃𝑧𝜑 ↔ ∃𝑧𝜓) |
3 | 2 | 2exbii 1851 | 1 ⊢ (∃𝑥∃𝑦∃𝑧𝜑 ↔ ∃𝑥∃𝑦∃𝑧𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∃wex 1781 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 |
This theorem depends on definitions: df-bi 206 df-ex 1782 |
This theorem is referenced by: 4exdistr 1965 ceqsex6v 3500 oprabidw 7382 oprabid 7383 dfoprab2 7409 dftpos3 8167 xpassen 8968 bnj916 33357 bnj917 33358 bnj983 33375 bnj996 33380 bnj1021 33390 bnj1033 33393 ellines 34675 rnxrn 36798 ichexmpl1 45562 |
Copyright terms: Public domain | W3C validator |