![]() |
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 3417 difin2 4255 resopab2 5994 ordtri3 6357 onunel 6426 resoprab2 7479 psgnran 19305 efgcpbllemb 19545 cndis 22665 cnindis 22666 cnpdis 22667 blpnf 23773 dscopn 23952 itgcn 25232 limcnlp 25265 2sqreultlem 26818 2sqreunnltlem 26821 dfcgrg2 27854 nb3gr2nb 28381 uspgr2wlkeq 28643 upgrspthswlk 28735 wspthsnwspthsnon 28910 wpthswwlks2on 28955 1stpreima 31674 cntzsnid 31959 qusxpid 32205 ressply1mon1p 32334 fsumcvg4 32595 mbfmcnt 32932 satfv0 34016 topdifinffinlem 35868 phpreu 36112 ptrest 36127 rngosn3 36433 isidlc 36524 dih1 39799 prjsperref 40991 lzunuz 41138 nadd1suc 41755 naddsuc2 41756 fsovrfovd 42373 uneqsn 42389 itsclquadeu 46953 pm4.71da 46965 i0oii 47042 io1ii 47043 |
Copyright terms: Public domain | W3C validator |