Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > pm4.71d | Structured version Visualization version Unicode 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 662 | . 2 | |
3 | 1, 2 | sylib 208 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 196 wa 384 |
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 386 |
This theorem is referenced by: difin2 3890 resopab2 5448 ordtri3 5759 fcnvres 6082 resoprab2 6757 psgnran 17935 efgcpbllemb 18168 cndis 21095 cnindis 21096 cnpdis 21097 blpnf 22202 dscopn 22378 itgcn 23609 limcnlp 23642 nb3gr2nb 26286 uspgr2wlkeq 26542 upgrspthswlk 26634 wspthsnwspthsnon 26811 wpthswwlks2on 26854 1stpreima 29484 fsumcvg4 29996 mbfmcnt 30330 topdifinffinlem 33195 phpreu 33393 ptrest 33408 rngosn3 33723 isidlc 33814 dih1 36575 lzunuz 37331 fsovrfovd 38303 uneqsn 38321 |
Copyright terms: Public domain | W3C validator |