![]() |
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 339 imim21b 393 pm5.74da 802 sbiedvw 2089 sbiedw 2305 dvelimdf 2443 sbied 2497 2mosOLD 2639 cbvraldva2 3332 csbie2df 4437 dfiin2g 5032 oneqmini 6420 tfindsg 7863 findsg 7902 brecop 8831 dom2lem 9015 indpi 10941 nn0ind-raph 12708 cncls2 23265 ismbl2 25544 voliunlem3 25569 mdbr2 32226 dmdbr2 32233 mdsl2i 32252 mdsl2bi 32253 sgn3da 34388 wl-dral1d 37239 wl-equsald 37247 wl-equsaldv 37248 cvlsupr3 39055 cdleme32fva 40149 cdlemk33N 40621 cdlemk34 40622 ralbidar 44156 logic1 48214 tfis2d 48462 |
Copyright terms: Public domain | W3C validator |