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 561 | . 2 ⊢ ((𝜓 → 𝜒) ↔ (𝜓 ↔ (𝜓 ∧ 𝜒))) | |
3 | 1, 2 | sylib 221 | 1 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: pm4.71rd 566 rabeqcda 3395 difin2 4192 resopab2 5889 ordtri3 6227 resoprab2 7307 psgnran 18861 efgcpbllemb 19099 cndis 22142 cnindis 22143 cnpdis 22144 blpnf 23249 dscopn 23425 itgcn 24696 limcnlp 24729 2sqreultlem 26282 2sqreunnltlem 26285 dfcgrg2 26908 nb3gr2nb 27426 uspgr2wlkeq 27687 upgrspthswlk 27779 wspthsnwspthsnon 27954 wpthswwlks2on 27999 1stpreima 30713 cntzsnid 30994 qusxpid 31227 fsumcvg4 31568 mbfmcnt 31901 satfv0 32987 onunel 33359 topdifinffinlem 35204 phpreu 35447 ptrest 35462 rngosn3 35768 isidlc 35859 dih1 38986 prjsperref 40094 lzunuz 40234 fsovrfovd 41235 uneqsn 41251 itsclquadeu 45739 pm4.71da 45751 i0oii 45829 io1ii 45830 |
Copyright terms: Public domain | W3C validator |