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 560 | . 2 ⊢ ((𝜓 → 𝜒) ↔ (𝜓 ↔ (𝜓 ∧ 𝜒))) | |
3 | 1, 2 | sylib 220 | 1 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 |
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 209 df-an 399 |
This theorem is referenced by: pm4.71rd 565 difin2 4266 resopab2 5904 ordtri3 6227 resoprab2 7271 psgnran 18643 efgcpbllemb 18881 cndis 21899 cnindis 21900 cnpdis 21901 blpnf 23007 dscopn 23183 itgcn 24443 limcnlp 24476 2sqreultlem 26023 2sqreunnltlem 26026 dfcgrg2 26649 nb3gr2nb 27166 uspgr2wlkeq 27427 upgrspthswlk 27519 wspthsnwspthsnon 27695 wpthswwlks2on 27740 1stpreima 30442 cntzsnid 30696 qusxpid 30928 fsumcvg4 31193 mbfmcnt 31526 satfv0 32605 topdifinffinlem 34631 phpreu 34891 ptrest 34906 rngosn3 35217 isidlc 35308 dih1 38437 rabeqcda 39126 prjsperref 39276 lzunuz 39385 fsovrfovd 40375 uneqsn 40393 itsclquadeu 44784 |
Copyright terms: Public domain | W3C validator |