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 231 | 1 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ 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 208 df-an 397 |
This theorem is referenced by: pm4.71ri 561 pm4.24 564 anabs1 658 pm4.45im 823 pm4.45 991 eu6lem 2654 2eu5 2738 2eu5OLD 2739 rabeqc 3677 imadmrn 5933 dff1o2 6614 f12dfv 7021 isof1oidb 7066 isof1oopb 7067 xpsnen 8590 dom0 8634 dfac5lem2 9539 pwfseqlem4 10073 axgroth6 10239 eqreznegel 12323 xrnemnf 12502 xrnepnf 12503 elioopnf 12821 elioomnf 12822 elicopnf 12823 elxrge0 12835 isprm2 16016 efgrelexlemb 18807 opsrtoslem1 20194 tgphaus 22654 cfilucfil3 23852 ioombl1lem4 24091 vitalilem1 24138 ellogdm 25149 nb3grpr2 27093 upgr2wlk 27378 erclwwlkref 27726 erclwwlknref 27776 0spth 27833 0crct 27840 pjimai 29881 dfrp2 30418 eulerpartlemt0 31527 bnj1101 31956 satfvsuclem2 32505 bj-snglc 34179 bj-epelb 34256 bj-opelidb1 34338 icorempo 34515 wl-cases2-dnf 34635 matunitlindf 34772 pm11.58 40602 |
Copyright terms: Public domain | W3C validator |