![]() |
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 663 | . 2 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 ↔ (𝜑 ∧ 𝜓))) | |
3 | 1, 2 | mpbi 220 | 1 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 |
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 197 df-an 385 |
This theorem is referenced by: pm4.24 676 pm4.45 724 anabs1 867 2eu5 2586 rabeqc 3394 imadmrn 5511 dff1o2 6180 f12dfv 6569 isof1oidb 6614 isof1oopb 6615 xpsnen 8085 dom0 8129 dfac5lem2 8985 pwfseqlem4 9522 axgroth6 9688 eqreznegel 11812 xrnemnf 11989 xrnepnf 11990 elioopnf 12305 elioomnf 12306 elicopnf 12307 elxrge0 12319 isprm2 15442 efgrelexlemb 18209 opsrtoslem1 19532 tgphaus 21967 cfilucfil3 23163 ioombl1lem4 23375 vitalilem1 23422 ellogdm 24430 nb3grpr2 26329 upgr2wlk 26620 erclwwlkref 26977 erclwwlknref 27033 0spth 27104 0crct 27111 pjimai 29163 dfrp2 29660 eulerpartlemt0 30559 bnj1101 30981 bj-snglc 33082 icorempt2 33329 wl-cases2-dnf 33425 matunitlindf 33537 pm11.58 38907 |
Copyright terms: Public domain | W3C validator |