![]() |
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 379. (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 412 | . 2 ⊢ (𝜑 → (𝜓 → 𝜃)) |
3 | pm5.21nd.2 | . . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) | |
4 | 3 | ex 412 | . 2 ⊢ (𝜑 → (𝜒 → 𝜃)) |
5 | pm5.21nd.3 | . . 3 ⊢ (𝜃 → (𝜓 ↔ 𝜒)) | |
6 | 5 | a1i 11 | . 2 ⊢ (𝜑 → (𝜃 → (𝜓 ↔ 𝜒))) |
7 | 2, 4, 6 | pm5.21ndd 379 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 |
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 207 df-an 396 |
This theorem is referenced by: ideqg 5864 fvelimab 6980 brrpssg 7743 ordsucelsuc 7841 releldm2 8066 relbrtpos 8260 relelec 8790 elfiun 9467 fpwwe2lem2 10669 fpwwelem 10682 fzrev3 13626 elfzp12 13639 eqgval 19207 ismhp 22161 eltg 22979 eltg2 22980 cncnp2 23304 isref 23532 islocfin 23540 opeldifid 32618 isfne 36321 copsex2b 37122 bj-ideqgALT 37140 bj-idreseq 37144 bj-ideqg1ALT 37147 opelopab3 37704 isdivrngo 37936 brssr 38482 islshpkrN 39101 dihatexv2 41321 |
Copyright terms: Public domain | W3C validator |