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 659 pm4.45im 825 pm4.45 995 eu6lem 2573 2eu5 2657 rabeqc 3622 dfid2 5491 imadmrn 5979 dff1o2 6721 f12dfv 7145 isof1oidb 7195 isof1oopb 7196 xpsnen 8842 dom0OLD 8890 dfac5lem2 9880 pwfseqlem4 10418 axgroth6 10584 eqreznegel 12674 xrnemnf 12853 xrnepnf 12854 dfrp2 13128 elioopnf 13175 elioomnf 13176 elicopnf 13177 elxrge0 13189 isprm2 16387 efgrelexlemb 19356 opsrtoslem1 21262 tgphaus 23268 cfilucfil3 24484 ioombl1lem4 24725 vitalilem1 24772 ellogdm 25794 nb3grpr2 27750 upgr2wlk 28036 erclwwlkref 28384 erclwwlknref 28433 0spth 28490 0crct 28497 pjimai 30538 eulerpartlemt0 32336 bnj1101 32764 satfvsuclem2 33322 bj-snglc 35159 bj-epelb 35240 bj-opelidb1 35324 icorempo 35522 wl-cases2-dnf 35671 matunitlindf 35775 pm11.58 42008 |
Copyright terms: Public domain | W3C validator |