![]() |
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 578 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))) |
3 | ancom 462 | . 2 ⊢ ((𝜒 ∧ 𝜓) ↔ (𝜓 ∧ 𝜒)) | |
4 | ancom 462 | . 2 ⊢ ((𝜃 ∧ 𝜓) ↔ (𝜓 ∧ 𝜃)) | |
5 | 2, 3, 4 | 3bitr4g 314 | 1 ⊢ (𝜑 → ((𝜒 ∧ 𝜓) ↔ (𝜃 ∧ 𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 |
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 206 df-an 398 |
This theorem is referenced by: anbi1d 631 pm5.71 1027 omord 8519 oeeui 8553 omxpenlem 9023 wemapwe 9641 fin23lem26 10269 1idpr 10973 repsdf2 14675 smueqlem 16378 tcphcph 24624 2sqreultlem 26818 2sqreunnltlem 26821 upgr2wlk 28665 upgrspthswlk 28735 isspthonpth 28746 iswwlksnx 28834 wwlksnextwrd 28891 rusgrnumwwlkl1 28962 isclwwlknx 29029 clwwlknwwlksnb 29048 clwwlknonel 29088 eupth2lem3lem6 29226 ordtconnlem1 32569 outsideofeu 34769 matunitlindf 36126 ftc1anclem6 36206 cvrval5 37928 cdleme0ex2N 38737 dihglb2 39855 mrefg2 41077 rmydioph 41385 islssfg2 41445 fsovrfovd 42373 elfz2z 45637 |
Copyright terms: Public domain | W3C validator |