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 rule). (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 259 | . 2 ⊢ ((𝜓 → (𝜒 ↔ 𝜃)) ↔ ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃))) | |
3 | 1, 2 | sylib 208 | 1 ⊢ (𝜑 → ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 |
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 197 |
This theorem is referenced by: imbi2d 330 imim21b 382 pm5.74da 723 cbval2 2279 cbvaldva 2281 dvelimdf 2335 sbied 2409 dfiin2g 4553 oneqmini 5776 tfindsg 7060 findsg 7093 brecop 7840 dom2lem 7995 indpi 9729 nn0ind-raph 11477 cncls2 21077 ismbl2 23295 voliunlem3 23320 mdbr2 29155 dmdbr2 29162 mdsl2i 29181 mdsl2bi 29182 sgn3da 30603 bj-cbval2v 32737 wl-dral1d 33318 wl-equsald 33325 cvlsupr3 34631 cdleme32fva 35725 cdlemk33N 36197 cdlemk34 36198 ralbidar 38649 tfis2d 42427 |
Copyright terms: Public domain | W3C validator |