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 383. (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 415 | . 2 ⊢ (𝜑 → (𝜓 → 𝜃)) |
3 | pm5.21nd.2 | . . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) | |
4 | 3 | ex 415 | . 2 ⊢ (𝜑 → (𝜒 → 𝜃)) |
5 | pm5.21nd.3 | . . 3 ⊢ (𝜃 → (𝜓 ↔ 𝜒)) | |
6 | 5 | a1i 11 | . 2 ⊢ (𝜑 → (𝜃 → (𝜓 ↔ 𝜒))) |
7 | 2, 4, 6 | pm5.21ndd 383 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 |
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 209 df-an 399 |
This theorem is referenced by: ideqg 5722 fvelimab 6737 brrpssg 7451 ordsucelsuc 7537 releldm2 7742 relbrtpos 7903 relelec 8334 elfiun 8894 fpwwe2lem2 10054 fpwwelem 10067 fzrev3 12974 elfzp12 12987 eqgval 18329 eltg 21565 eltg2 21566 cncnp2 21889 isref 22117 islocfin 22125 opeldifid 30349 isfne 33687 copsex2b 34435 bj-ideqgALT 34453 bj-idreseq 34457 bj-ideqg1ALT 34460 opelopab3 35007 isdivrngo 35243 brssr 35756 islshpkrN 36271 dihatexv2 38490 |
Copyright terms: Public domain | W3C validator |