![]() |
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 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: anabs7 662 biadaniALT 819 orabs 997 prlem2 1054 dfeumo 2531 dfeu 2589 2moswapv 2625 2moswap 2640 exsnrex 4683 eliunxp 5835 asymref 6114 imaindm 6295 dffun9 6574 funcnv 6614 funcnv3 6615 f1ompt 7107 eufnfv 7227 dff1o6 7269 dfom2 7853 elxp4 7909 elxp5 7910 abexex 7954 dfoprab4 8037 tpostpos 8227 brwitnlem 8503 erovlem 8803 elixp2 8891 xpsnen 9051 elom3 9639 ttrclse 9718 cardval2 9982 isinfcard 10083 infmap2 10209 elznn0nn 12568 zrevaddcl 12603 qrevaddcl 12951 hash2prb 14429 cotr2g 14919 climreu 15496 isprm3 16616 hashbc0 16934 imasleval 17483 xpscf 17507 isssc 17763 issubmndb 18682 isgim 19130 eldprd 19868 brric2 20277 islmim 20665 tgval2 22450 eltg2b 22453 snfil 23359 isms2 23947 setsms 23979 elii1 24442 phtpcer 24502 elovolm 24983 ellimc2 25385 limcun 25403 1cubr 26336 fsumvma2 26706 dchrelbas3 26730 2lgslem1b 26884 dmscut 27301 madeval2 27337 made0 27357 nbgrel 28586 rusgrnumwwlks 29217 isgrpo 29737 mdsl2i 31562 cvmdi 31564 rabfmpunirn 31865 zarcls 32842 eulerpartlemn 33368 bnj580 33912 bnj1049 33973 snmlval 34310 satf0suclem 34354 fmlasuc0 34363 elmthm 34555 brtxp2 34841 brpprod3a 34846 bj-elid6 36039 ismgmOLD 36706 brres2 37124 brxrn2 37233 redundpim3 37488 prtlem100 37717 islln2 38370 islpln2 38395 islvol2 38439 prjspeclsp 41350 onsucrn 42006 dflim5 42064 en2pr 42283 pren2 42289 elmapintrab 42312 clcnvlem 42359 sprvalpw 46134 sprvalpwn0 46137 prprvalpw 46169 eliunxp2 46962 elbigo 47190 |
Copyright terms: Public domain | W3C validator |