Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > pm5.32rd | Structured version Visualization version GIF version |
Description: Distribution of implication over biconditional (deduction form). (Contributed by NM, 25-Dec-2004.) |
Ref | Expression |
---|---|
pm5.32d.1 | ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))) |
Ref | Expression |
---|---|
pm5.32rd | ⊢ (𝜑 → ((𝜒 ∧ 𝜓) ↔ (𝜃 ∧ 𝜓))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm5.32d.1 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))) | |
2 | 1 | pm5.32d 580 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))) |
3 | ancom 464 | . 2 ⊢ ((𝜒 ∧ 𝜓) ↔ (𝜓 ∧ 𝜒)) | |
4 | ancom 464 | . 2 ⊢ ((𝜃 ∧ 𝜓) ↔ (𝜓 ∧ 𝜃)) | |
5 | 2, 3, 4 | 3bitr4g 317 | 1 ⊢ (𝜑 → ((𝜒 ∧ 𝜓) ↔ (𝜃 ∧ 𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: anbi1d 633 pm5.71 1028 omord 8296 oeeui 8330 omxpenlem 8746 wemapwe 9312 fin23lem26 9939 1idpr 10643 repsdf2 14343 smueqlem 16049 tcphcph 24134 2sqreultlem 26328 2sqreunnltlem 26331 upgr2wlk 27756 upgrspthswlk 27825 isspthonpth 27836 iswwlksnx 27924 wwlksnextwrd 27981 rusgrnumwwlkl1 28052 isclwwlknx 28119 clwwlknwwlksnb 28138 clwwlknonel 28178 eupth2lem3lem6 28316 ordtconnlem1 31588 outsideofeu 34170 matunitlindf 35512 ftc1anclem6 35592 cvrval5 37166 cdleme0ex2N 37975 dihglb2 39093 mrefg2 40232 rmydioph 40539 islssfg2 40599 fsovrfovd 41294 elfz2z 44480 |
Copyright terms: Public domain | W3C validator |