![]() |
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 558 | . 2 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 ↔ (𝜑 ∧ 𝜓))) | |
3 | 1, 2 | mpbi 229 | 1 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ 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 206 df-an 397 |
This theorem is referenced by: pm4.71ri 561 pm4.24 564 anabs1 660 pm4.45im 826 pm4.45 996 eu6lem 2567 2eu5 2651 rabeqcOLD 3680 dfid2 5575 imadmrn 6067 dff1o2 6835 f12dfv 7267 isof1oidb 7317 isof1oopb 7318 xpsnen 9051 dom0OLD 9099 dfac5lem2 10115 pwfseqlem4 10653 axgroth6 10819 eqreznegel 12914 xrnemnf 13093 xrnepnf 13094 dfrp2 13369 elioopnf 13416 elioomnf 13417 elicopnf 13418 elxrge0 13430 isprm2 16615 efgrelexlemb 19612 opsrtoslem1 21607 tgphaus 23612 cfilucfil3 24828 ioombl1lem4 25069 vitalilem1 25116 ellogdm 26138 nb3grpr2 28629 upgr2wlk 28914 erclwwlkref 29262 erclwwlknref 29311 0spth 29368 0crct 29375 pjimai 31416 eulerpartlemt0 33356 bnj1101 33783 satfvsuclem2 34339 bj-snglc 35838 bj-epelb 35938 bj-opelidb1 36022 icorempo 36220 wl-cases2-dnf 36369 matunitlindf 36474 disjressuc2 37246 dflim5 42064 pm11.58 43134 |
Copyright terms: Public domain | W3C validator |