| 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 559 | . 2 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜓)) |
| 3 | 2 | biancomi 462 | 1 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜑)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 |
| 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 207 df-an 396 |
| This theorem is referenced by: anabs7 664 biadaniALT 821 orabs 1001 prlem2 1056 dfeumo 2537 dfeu 2595 2moswapv 2629 2moswap 2644 exsnrex 4680 eliunxp 5848 asymref 6136 imaindm 6319 dffun9 6595 funcnv 6635 funcnv3 6636 f1ompt 7131 eufnfv 7249 dff1o6 7295 dfom2 7889 elxp4 7944 elxp5 7945 abexex 7996 dfoprab4 8080 tpostpos 8271 brwitnlem 8545 erovlem 8853 elixp2 8941 xpsnen 9095 elom3 9688 ttrclse 9767 cardval2 10031 isinfcard 10132 infmap2 10257 elznn0nn 12627 zrevaddcl 12662 qrevaddcl 13013 hash2prb 14511 hash3tpb 14534 cotr2g 15015 climreu 15592 isprm3 16720 hashbc0 17043 imasleval 17586 xpscf 17610 isssc 17864 issubmndb 18818 isgim 19280 eldprd 20024 brric2 20506 islmim 21061 tgval2 22963 eltg2b 22966 snfil 23872 isms2 24460 setsms 24492 elii1 24964 phtpcer 25027 elovolm 25510 ellimc2 25912 limcun 25930 1cubr 26885 fsumvma2 27258 dchrelbas3 27282 2lgslem1b 27436 dmscut 27856 madeval2 27892 made0 27912 nbgrel 29357 rusgrnumwwlks 29994 isgrpo 30516 mdsl2i 32341 cvmdi 32343 rabfmpunirn 32663 zarcls 33873 eulerpartlemn 34383 bnj580 34927 bnj1049 34988 snmlval 35336 satf0suclem 35380 fmlasuc0 35389 elmthm 35581 brtxp2 35882 brpprod3a 35887 bj-elid6 37171 ismgmOLD 37857 brres2 38269 brxrn2 38376 redundpim3 38631 prtlem100 38860 islln2 39513 islpln2 39538 islvol2 39582 prjspeclsp 42622 onsucrn 43284 dflim5 43342 en2pr 43560 pren2 43566 elmapintrab 43589 clcnvlem 43636 sprvalpw 47467 sprvalpwn0 47470 prprvalpw 47502 clnbgrel 47815 eliunxp2 48250 elbigo 48472 |
| Copyright terms: Public domain | W3C validator |