![]() |
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 559 | . 2 ⊢ ((𝜓 → 𝜒) ↔ (𝜓 ↔ (𝜓 ∧ 𝜒))) | |
3 | 1, 2 | sylib 217 | 1 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 |
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 df-an 398 |
This theorem is referenced by: pm4.71rd 564 rabeqcda 3444 difin2 4289 resopab2 6033 ordtri3 6396 onunel 6465 resoprab2 7521 psgnran 19375 efgcpbllemb 19615 cndis 22776 cnindis 22777 cnpdis 22778 blpnf 23884 dscopn 24063 itgcn 25343 limcnlp 25376 2sqreultlem 26929 2sqreunnltlem 26932 dfcgrg2 28093 nb3gr2nb 28620 uspgr2wlkeq 28882 upgrspthswlk 28974 wspthsnwspthsnon 29149 wpthswwlks2on 29194 1stpreima 31905 cntzsnid 32190 qusxpid 32443 qsfld 32564 ressply1mon1p 32603 fsumcvg4 32867 mbfmcnt 33204 satfv0 34286 topdifinffinlem 36165 phpreu 36409 ptrest 36424 rngosn3 36729 isidlc 36820 dih1 40094 prjsperref 41291 lzunuz 41438 nadd1suc 42074 naddsuc2 42075 fsovrfovd 42692 uneqsn 42708 itsclquadeu 47364 pm4.71da 47376 i0oii 47453 io1ii 47454 |
Copyright terms: Public domain | W3C validator |