![]() |
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 269 | . 2 ⊢ ((𝜓 → (𝜒 ↔ 𝜃)) ↔ ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃))) | |
3 | 1, 2 | sylib 217 | 1 ⊢ (𝜑 → ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 |
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 |
This theorem is referenced by: imbi2d 340 imim21b 395 pm5.74da 802 sbiedvw 2096 sbiedw 2310 dvelimdf 2448 sbied 2506 2mos 2650 cbvraldva2 3321 csbie2df 4398 dfiin2g 4990 oneqmini 6367 tfindsg 7789 findsg 7828 brecop 8707 dom2lem 8890 indpi 10801 nn0ind-raph 12561 cncls2 22576 ismbl2 24843 voliunlem3 24868 mdbr2 31067 dmdbr2 31074 mdsl2i 31093 mdsl2bi 31094 sgn3da 32953 wl-dral1d 35928 wl-equsald 35936 cvlsupr3 37744 cdleme32fva 38838 cdlemk33N 39310 cdlemk34 39311 ralbidar 42636 logic1 46777 tfis2d 47026 |
Copyright terms: Public domain | W3C validator |