![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pm4.71ri | Structured version Visualization version Unicode 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 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | pm4.71r 641 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mpbi 213 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
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 190 df-an 377 |
This theorem is referenced by: biadan2 652 anabs7 824 orabs 871 prlem2 980 eu5 2335 2moswap 2386 exsnrex 4020 eliunxp 4990 asymref 5234 dffun9 5628 funcnv 5664 funcnv3 5665 f1ompt 6066 eufnfv 6163 dff1o6 6198 dfom2 6720 elxp4 6763 elxp5 6764 abexex 6802 dfoprab4 6876 tpostpos 7018 brwitnlem 7234 erovlem 7484 elixp2 7551 xpsnen 7681 elom3 8178 cardval2 8450 isinfcard 8548 infmap2 8673 elznn0nn 10979 zrevaddcl 11010 qrevaddcl 11314 hash2prb 12665 cotr2g 13088 climreu 13668 isprm3 14681 hashbc0 15005 imasleval 15495 isssc 15773 isgim 16974 eldprd 17684 brric2 18021 islmim 18333 tgval2 20019 eltg2b 20022 snfil 20927 isms2 21513 setsms 21543 elii1 22011 phtpcer 22074 elovolm 22476 ellimc2 22880 limcun 22898 1cubr 23816 fsumvma2 24190 dchrelbas3 24214 rusgranumwlks 25732 isgrpo 25972 issubgo 26079 ismgmOLD 26096 mdsl2i 28023 cvmdi 28025 rabfmpunirn 28300 eulerpartlemn 29262 bnj580 29772 bnj1049 29831 snmlval 30102 elmthm 30262 brtxp2 30696 brpprod3a 30701 prtlem100 32473 islln2 33120 islpln2 33145 islvol2 33189 elmapintrab 36226 clcnvlem 36274 eliunxp2 40387 elbigo 40634 |
Copyright terms: Public domain | W3C validator |