Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > pm4.71d | Structured version Visualization version GIF version |
Description: Deduction converting an implication to a biconditional with conjunction. Deduction from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by Mario Carneiro, 25-Dec-2016.) |
Ref | Expression |
---|---|
pm4.71rd.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
pm4.71d | ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm4.71rd.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | pm4.71 660 | . 2 ⊢ ((𝜓 → 𝜒) ↔ (𝜓 ↔ (𝜓 ∧ 𝜒))) | |
3 | 1, 2 | sylib 207 | 1 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 |
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 196 df-an 385 |
This theorem is referenced by: difin2 3849 resopab2 5368 ordtri3 5676 fcnvres 5995 resoprab2 6655 psgnran 17758 efgcpbllemb 17991 cndis 20905 cnindis 20906 cnpdis 20907 blpnf 22012 dscopn 22188 itgcn 23415 limcnlp 23448 nb3gra2nb 25984 usg2wlkeq 26236 clwwlkn2 26303 1stpreima 28867 fsumcvg4 29324 mbfmcnt 29657 topdifinffinlem 32371 phpreu 32563 ptrest 32578 rngosn3 32893 isidlc 32984 dih1 35593 lzunuz 36349 fsovrfovd 37323 uneqsn 37341 nb3gr2nb 40612 uspgr2wlkeq 40854 upgrspths1wlk 40944 wspthsnwspthsnon 41122 wpthswwlks2on 41164 |
Copyright terms: Public domain | W3C validator |