![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pm4.71rd | Structured version Visualization version Unicode version |
Description: Deduction converting an implication to a biconditional with conjunction. Deduction from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 10-Feb-2005.) |
Ref | Expression |
---|---|
pm4.71rd.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
pm4.71rd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm4.71rd.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | pm4.71r 637 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sylib 200 |
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 189 df-an 373 |
This theorem is referenced by: 2reu5 3248 ralss 3495 rexss 3496 reuhypd 4627 exopxfr2 4979 dfco2a 5335 feu 5759 funbrfv2b 5909 dffn5 5910 eqfnfv2 5977 dff4 6036 fmptco 6056 dff13 6159 opiota 6852 mpt2xopovel 6966 brtpos 6982 dftpos3 6991 erinxp 7437 qliftfun 7448 pw2f1olem 7676 infm3 10568 prime 11016 predfz 11914 hashf1lem2 12619 smueqlem 14464 vdwmc2 14929 acsfiel 15560 subsubc 15758 ismgmid 16507 eqger 16867 eqgid 16869 gaorber 16962 symgfix2 17057 psrbaglefi 18596 znleval 19125 bastop2 20010 elcls2 20090 maxlp 20163 restopn2 20193 restdis 20194 1stccn 20478 tx1cn 20624 tx2cn 20625 imasnopn 20705 imasncld 20706 imasncls 20707 idqtop 20721 tgqtop 20727 filuni 20900 uffix2 20939 cnflf 21017 isfcls 21024 fclsopn 21029 cnfcf 21057 ptcmplem2 21068 xmeter 21448 imasf1oxms 21504 prdsbl 21506 caucfil 22253 cfilucfil4 22289 shft2rab 22461 sca2rab 22465 mbfinf 22621 mbfinfOLD 22622 i1f1lem 22647 i1fres 22663 itg1climres 22672 mbfi1fseqlem4 22676 iblpos 22750 itgposval 22753 cnplimc 22842 ply1remlem 23113 plyremlem 23257 dvdsflsumcom 24117 fsumvma2 24142 vmasum 24144 logfac2 24145 chpchtsum 24147 logfaclbnd 24150 lgsquadlem1 24282 lgsquadlem2 24283 lgsquadlem3 24284 dchrisum0lem1 24354 colinearalg 24940 nbgrael 25154 nbgraeledg 25158 nbgraf1olem1 25169 2spot2iun2spont 25619 eupath2lem2 25706 eupath2 25708 frgraeu 25782 usgreg2spot 25795 pjpreeq 27051 elnlfn 27581 fimarab 28244 feqmptdf 28258 fmptcof2 28259 dfcnv2 28279 2ndpreima 28288 f1od2 28309 fpwrelmap 28318 iocinioc2 28361 nndiffz1 28366 indpi1 28843 1stmbfm 29082 2ndmbfm 29083 eulerpartlemgh 29211 bnj1171 29809 mrsubrn 30151 elfuns 30682 fneval 31008 topdifinfindis 31749 phpreu 31929 poimirlem23 31963 poimirlem26 31966 poimirlem27 31967 areacirclem5 32036 prter3 32454 islshpat 32583 lfl1dim 32687 glbconxN 32943 cdlemefrs29bpre0 33963 dib1dim 34733 dib1dim2 34736 diclspsn 34762 dihopelvalcpre 34816 dih1dimatlem 34897 mapdordlem1a 35202 hdmapoc 35502 rmydioph 35869 pw2f1ocnv 35892 funbrafv2b 38661 dfafn5a 38662 nbgrel 39410 nbusgreledg 39421 nbusgredgeu0 39442 umgr2v2enb1 39563 |
Copyright terms: Public domain | W3C validator |