![]() |
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 262 | . 2 ⊢ ((𝜓 → (𝜒 ↔ 𝜃)) ↔ ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃))) | |
3 | 1, 2 | sylib 210 | 1 ⊢ (𝜑 → ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 |
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 199 |
This theorem is referenced by: imbi2d 333 imim21b 386 pm5.74da 791 cbval2OLD 2344 dvelimdf 2383 sbied 2467 sbiedALT 2538 2mos 2675 cbvraldva2 3381 cbvrexdva2OLD 3383 dfiin2g 4821 oneqmini 6074 tfindsg 7385 findsg 7418 brecop 8182 dom2lem 8338 indpi 10119 nn0ind-raph 11888 cncls2 21575 ismbl2 23821 voliunlem3 23846 mdbr2 29844 dmdbr2 29851 mdsl2i 29870 mdsl2bi 29871 sgn3da 31402 bj-cbval2v 33522 wl-dral1d 34149 wl-equsald 34157 cvlsupr3 35873 cdleme32fva 36966 cdlemk33N 37438 cdlemk34 37439 ralbidar 40140 tfis2d 44090 |
Copyright terms: Public domain | W3C validator |