| 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 557 | . 2 ⊢ ((𝜓 → 𝜒) ↔ (𝜓 ↔ (𝜓 ∧ 𝜒))) | |
| 3 | 1, 2 | sylib 218 | 1 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜒))) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 |
| 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 207 df-an 396 |
| This theorem is referenced by: pm4.71rd 562 rabeqcda 3448 difin2 4301 resopab2 6054 ordtri3 6420 onunel 6489 resoprab2 7552 naddsuc2 8739 psgnran 19533 efgcpbllemb 19773 cndis 23299 cnindis 23300 cnpdis 23301 blpnf 24407 dscopn 24586 itgcn 25880 limcnlp 25913 2sqreultlem 27491 2sqreunnltlem 27494 dfcgrg2 28871 nb3gr2nb 29401 uspgr2wlkeq 29664 upgrspthswlk 29758 wspthsnwspthsnon 29936 wpthswwlks2on 29981 1stpreima 32716 cntzsnid 33072 erler 33269 qusxpid 33391 qsfld 33526 ressply1mon1p 33593 fsumcvg4 33949 mbfmcnt 34270 satfv0 35363 topdifinffinlem 37348 phpreu 37611 ptrest 37626 rngosn3 37931 isidlc 38022 dih1 41288 redvmptabs 42390 prjsperref 42616 lzunuz 42779 nadd1suc 43405 fsovrfovd 44022 uneqsn 44038 itsclquadeu 48698 pm4.71da 48710 i0oii 48817 io1ii 48818 |
| Copyright terms: Public domain | W3C validator |