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 561 | . 2 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 ↔ (𝜑 ∧ 𝜓))) | |
3 | 1, 2 | mpbi 233 | 1 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: pm4.71ri 564 pm4.24 567 anabs1 662 pm4.45im 827 pm4.45 997 eu6lem 2575 2eu5 2659 rabeqc 3591 imadmrn 5923 dff1o2 6635 f12dfv 7053 isof1oidb 7102 isof1oopb 7103 xpsnen 8662 dom0 8707 dfac5lem2 9636 pwfseqlem4 10174 axgroth6 10340 eqreznegel 12428 xrnemnf 12607 xrnepnf 12608 dfrp2 12882 elioopnf 12929 elioomnf 12930 elicopnf 12931 elxrge0 12943 isprm2 16135 efgrelexlemb 19006 opsrtoslem1 20878 tgphaus 22880 cfilucfil3 24084 ioombl1lem4 24325 vitalilem1 24372 ellogdm 25394 nb3grpr2 27337 upgr2wlk 27622 erclwwlkref 27969 erclwwlknref 28018 0spth 28075 0crct 28082 pjimai 30123 eulerpartlemt0 31918 bnj1101 32347 satfvsuclem2 32905 bj-snglc 34814 bj-epelb 34894 bj-opelidb1 34977 icorempo 35177 wl-cases2-dnf 35326 matunitlindf 35430 pm11.58 41586 |
Copyright terms: Public domain | W3C validator |