Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > pm4.71ri | 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 (with conjunct reversed). (Contributed by NM, 1-Dec-2003.) |
Ref | Expression |
---|---|
pm4.71ri.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
pm4.71ri | ⊢ (𝜑 ↔ (𝜓 ∧ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm4.71ri.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | pm4.71i 560 | . 2 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜓)) |
3 | 2 | biancomi 463 | 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: anabs7 660 biadaniALT 817 orabs 992 prlem2 1047 dfeumo 2612 dfeu 2674 2moswapv 2707 2moswap 2722 exsnrex 4610 eliunxp 5701 asymref 5969 dffun9 6377 funcnv 6416 funcnv3 6417 f1ompt 6867 eufnfv 6982 dff1o6 7023 dfom2 7571 elxp4 7616 elxp5 7617 abexex 7661 dfoprab4 7742 tpostpos 7901 brwitnlem 8121 erovlem 8382 elixp2 8453 xpsnen 8589 elom3 9099 cardval2 9408 isinfcard 9506 infmap2 9628 elznn0nn 11983 zrevaddcl 12015 qrevaddcl 12358 hash2prb 13818 cotr2g 14324 climreu 14901 isprm3 16015 hashbc0 16329 imasleval 16802 xpscf 16826 isssc 17078 issubmndb 17958 isgim 18340 eldprd 19055 brric2 19429 islmim 19763 tgval2 21492 eltg2b 21495 snfil 22400 isms2 22987 setsms 23017 elii1 23466 phtpcer 23526 elovolm 24003 ellimc2 24402 limcun 24420 1cubr 25347 fsumvma2 25717 dchrelbas3 25741 2lgslem1b 25895 nbgrel 27049 rusgrnumwwlks 27680 isgrpo 28201 mdsl2i 30026 cvmdi 30028 rabfmpunirn 30326 eulerpartlemn 31538 bnj580 32084 bnj1049 32143 snmlval 32475 satf0suclem 32519 fmlasuc0 32528 elmthm 32720 imaindm 32919 dmscut 33169 madeval2 33187 brtxp2 33239 brpprod3a 33244 bj-elid6 34354 ismgmOLD 35009 brres2 35410 brxrn2 35507 redundpim3 35745 prtlem100 35875 islln2 36527 islpln2 36552 islvol2 36596 prjspeclsp 39140 en2pr 39784 pren2 39790 elmapintrab 39814 clcnvlem 39861 sprvalpw 43519 sprvalpwn0 43522 prprvalpw 43554 eliunxp2 44310 elbigo 44539 |
Copyright terms: Public domain | W3C validator |