| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > pm4.71i | Structured version Visualization version GIF version | ||
| Description: Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 4-Jan-2004.) |
| Ref | Expression |
|---|---|
| pm4.71i.1 | ⊢ (𝜑 → 𝜓) |
| Ref | Expression |
|---|---|
| pm4.71i | ⊢ (𝜑 ↔ (𝜑 ∧ 𝜓)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pm4.71i.1 | . 2 ⊢ (𝜑 → 𝜓) | |
| 2 | pm4.71 557 | . 2 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 ↔ (𝜑 ∧ 𝜓))) | |
| 3 | 1, 2 | mpbi 230 | 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.71ri 560 pm4.24 563 anabs1 662 pm4.45im 828 pm4.45 1000 eu6lem 2573 2eu5 2656 rabeqcOLD 3690 dfid2 5580 imadmrn 6088 dff1o2 6853 f12dfv 7293 isof1oidb 7344 isof1oopb 7345 xpsnen 9095 dom0OLD 9143 dfac5lem2 10164 axgroth6 10868 eqreznegel 12976 xrnemnf 13159 xrnepnf 13160 dfrp2 13436 elioopnf 13483 elioomnf 13484 elicopnf 13485 elxrge0 13497 isprm2 16719 efgrelexlemb 19768 opsrtoslem1 22079 tgphaus 24125 cfilucfil3 25354 ioombl1lem4 25596 vitalilem1 25643 ellogdm 26681 nb3grpr2 29400 upgr2wlk 29686 erclwwlkref 30039 erclwwlknref 30088 0spth 30145 0crct 30152 pjimai 32195 eulerpartlemt0 34371 bnj1101 34798 satfvsuclem2 35365 bj-snglc 36970 bj-epelb 37070 bj-opelidb1 37154 icorempo 37352 wl-cases2-dnf 37513 matunitlindf 37625 disjressuc2 38389 dflim5 43342 pm11.58 44409 |
| Copyright terms: Public domain | W3C validator |