![]() |
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 558 | . 2 ⊢ ((𝜓 → 𝜒) ↔ (𝜓 ↔ (𝜓 ∧ 𝜒))) | |
3 | 1, 2 | sylib 219 | 1 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: pm4.71rd 563 difin2 4192 resopab2 5792 ordtri3 6109 resoprab2 7134 psgnran 18378 efgcpbllemb 18612 cndis 21587 cnindis 21588 cnpdis 21589 blpnf 22694 dscopn 22870 itgcn 24130 limcnlp 24163 2sqreultlem 25709 2sqreunnltlem 25712 dfcgrg2 26336 nb3gr2nb 26853 uspgr2wlkeq 27114 upgrspthswlk 27205 wspthsnwspthsnon 27381 wpthswwlks2on 27426 1stpreima 30126 cntzsnid 30503 fsumcvg4 30806 mbfmcnt 31139 satfv0 32215 topdifinffinlem 34180 phpreu 34428 ptrest 34443 rngosn3 34755 isidlc 34846 dih1 37974 rabeqcda 38657 prjsperref 38774 lzunuz 38871 fsovrfovd 39861 uneqsn 39879 itsclquadeu 44267 |
Copyright terms: Public domain | W3C validator |