Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > pm5.74d | Structured version Visualization version GIF version |
Description: Distribution of implication over biconditional (deduction form). (Contributed by NM, 21-Mar-1996.) |
Ref | Expression |
---|---|
pm5.74d.1 | ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))) |
Ref | Expression |
---|---|
pm5.74d | ⊢ (𝜑 → ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm5.74d.1 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))) | |
2 | pm5.74 273 | . 2 ⊢ ((𝜓 → (𝜒 ↔ 𝜃)) ↔ ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃))) | |
3 | 1, 2 | sylib 221 | 1 ⊢ (𝜑 → ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 |
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 |
This theorem is referenced by: imbi2d 344 imim21b 398 pm5.74da 804 sbiedvw 2100 sbiedw 2314 sbiedwOLD 2315 cbval2vOLD 2344 dvelimdf 2448 sbied 2506 2mos 2650 cbvraldva2 3367 csbie2df 4355 dfiin2g 4941 oneqmini 6264 tfindsg 7639 findsg 7677 brecop 8492 dom2lem 8668 indpi 10521 nn0ind-raph 12277 cncls2 22170 ismbl2 24424 voliunlem3 24449 mdbr2 30377 dmdbr2 30384 mdsl2i 30403 mdsl2bi 30404 sgn3da 32220 wl-dral1d 35427 wl-equsald 35435 cvlsupr3 37095 cdleme32fva 38188 cdlemk33N 38660 cdlemk34 38661 ralbidar 41736 logic1 45809 tfis2d 46057 |
Copyright terms: Public domain | W3C validator |