![]() |
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 547 | . 2 ⊢ ((𝜓 → 𝜒) ↔ (𝜓 ↔ (𝜓 ∧ 𝜒))) | |
3 | 1, 2 | sylib 208 | 1 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 382 |
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 df-an 383 |
This theorem is referenced by: difin2 4038 resopab2 5587 ordtri3 5900 fcnvres 6220 resoprab2 6904 psgnran 18138 efgcpbllemb 18371 cndis 21312 cnindis 21313 cnpdis 21314 blpnf 22418 dscopn 22594 itgcn 23825 limcnlp 23858 nb3gr2nb 26505 uspgr2wlkeq 26773 upgrspthswlk 26865 wspthsnwspthsnon 27057 wspthsnwspthsnonOLD 27059 wpthswwlks2on 27105 wpthswwlks2onOLD 27106 1stpreima 29820 fsumcvg4 30332 mbfmcnt 30666 topdifinffinlem 33528 phpreu 33722 ptrest 33737 rngosn3 34051 isidlc 34142 dih1 37093 lzunuz 37854 fsovrfovd 38826 uneqsn 38844 |
Copyright terms: Public domain | W3C validator |