|   | 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 5862 fvelimab 6981 brrpssg 7745 ordsucelsuc 7842 releldm2 8068 relbrtpos 8262 relelec 8792 elfiun 9470 fpwwe2lem2 10672 fpwwelem 10685 fzrev3 13630 elfzp12 13643 eqgval 19195 ismhp 22144 eltg 22964 eltg2 22965 cncnp2 23289 isref 23517 islocfin 23525 opeldifid 32612 isfne 36340 copsex2b 37141 bj-ideqgALT 37159 bj-idreseq 37163 bj-ideqg1ALT 37166 opelopab3 37725 isdivrngo 37957 brssr 38502 islshpkrN 39121 dihatexv2 41341 | 
| Copyright terms: Public domain | W3C validator |