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 577 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))) |
3 | ancom 461 | . 2 ⊢ ((𝜒 ∧ 𝜓) ↔ (𝜓 ∧ 𝜒)) | |
4 | ancom 461 | . 2 ⊢ ((𝜃 ∧ 𝜓) ↔ (𝜓 ∧ 𝜃)) | |
5 | 2, 3, 4 | 3bitr4g 315 | 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: anbi1d 629 pm5.71 1021 omord 8183 oeeui 8217 omxpenlem 8606 wemapwe 9148 fin23lem26 9735 1idpr 10439 repsdf2 14128 smueqlem 15827 tcphcph 23767 2sqreultlem 25950 2sqreunnltlem 25953 upgr2wlk 27377 upgrspthswlk 27446 isspthonpth 27457 iswwlksnx 27545 wwlksnextwrd 27602 rusgrnumwwlkl1 27674 isclwwlknx 27741 clwwlknwwlksnb 27761 clwwlknonel 27801 eupth2lem3lem6 27939 ordtconnlem1 31066 outsideofeu 33489 matunitlindf 34771 ftc1anclem6 34853 cvrval5 36431 cdleme0ex2N 37240 dihglb2 38358 mrefg2 39182 rmydioph 39489 islssfg2 39549 fsovrfovd 40233 elfz2z 43392 |
Copyright terms: Public domain | W3C validator |