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 1839 | . 2 ⊢ (∃𝑧𝜑 ↔ ∃𝑧𝜓) |
3 | 2 | 2exbii 1840 | 1 ⊢ (∃𝑥∃𝑦∃𝑧𝜑 ↔ ∃𝑥∃𝑦∃𝑧𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 ∃wex 1771 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 |
This theorem depends on definitions: df-bi 208 df-ex 1772 |
This theorem is referenced by: 4exdistr 1954 ceqsex6v 3545 oprabidw 7176 oprabid 7177 dfoprab2 7201 dftpos3 7899 xpassen 8599 bnj916 32104 bnj917 32105 bnj983 32122 bnj996 32126 bnj1021 32135 bnj1033 32138 ellines 33510 rnxrn 35526 ichexmpl1 43508 |
Copyright terms: Public domain | W3C validator |