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 8184 oeeui 8218 omxpenlem 8607 wemapwe 9149 fin23lem26 9736 1idpr 10440 repsdf2 14130 smueqlem 15829 tcphcph 23769 2sqreultlem 25951 2sqreunnltlem 25954 upgr2wlk 27378 upgrspthswlk 27447 isspthonpth 27458 iswwlksnx 27546 wwlksnextwrd 27603 rusgrnumwwlkl1 27675 isclwwlknx 27742 clwwlknwwlksnb 27762 clwwlknonel 27802 eupth2lem3lem6 27940 ordtconnlem1 31067 outsideofeu 33490 matunitlindf 34772 ftc1anclem6 34854 cvrval5 36433 cdleme0ex2N 37242 dihglb2 38360 mrefg2 39184 rmydioph 39491 islssfg2 39551 fsovrfovd 40235 elfz2z 43396 |
Copyright terms: Public domain | W3C validator |