![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pm5.21nd | Structured version Visualization version GIF version |
Description: Eliminate an antecedent implied by each side of a biconditional. Variant of pm5.21ndd 381. (Contributed by NM, 20-Nov-2005.) (Proof shortened by Wolf Lammen, 4-Nov-2013.) |
Ref | Expression |
---|---|
pm5.21nd.1 | ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
pm5.21nd.2 | ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
pm5.21nd.3 | ⊢ (𝜃 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
pm5.21nd | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm5.21nd.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) | |
2 | 1 | ex 413 | . 2 ⊢ (𝜑 → (𝜓 → 𝜃)) |
3 | pm5.21nd.2 | . . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) | |
4 | 3 | ex 413 | . 2 ⊢ (𝜑 → (𝜒 → 𝜃)) |
5 | pm5.21nd.3 | . . 3 ⊢ (𝜃 → (𝜓 ↔ 𝜒)) | |
6 | 5 | a1i 11 | . 2 ⊢ (𝜑 → (𝜃 → (𝜓 ↔ 𝜒))) |
7 | 2, 4, 6 | pm5.21ndd 381 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 208 df-an 397 |
This theorem is referenced by: ideqg 5600 fvelimab 6597 brrpssg 7300 ordsucelsuc 7384 releldm2 7589 relbrtpos 7745 relelec 8175 elfiun 8730 fpwwe2lem2 9889 fpwwelem 9902 fzrev3 12812 elfzp12 12825 eqgval 18070 eltg 21237 eltg2 21238 cncnp2 21561 isref 21789 islocfin 21797 opeldifid 30015 isfne 33241 opelopab3 34470 isdivrngo 34706 brssr 35222 islshpkrN 35737 dihatexv2 37956 |
Copyright terms: Public domain | W3C validator |