![]() |
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 643 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sylib 201 |
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 378 |
This theorem is referenced by: 2reu5 3236 ralss 3481 rexss 3482 reuhypd 4627 exopxfr2 4984 dfco2a 5342 feu 5771 funbrfv2b 5923 dffn5 5924 feqmptdf 5934 eqfnfv2 5992 dff4 6051 fmptco 6072 dff13 6177 opiota 6871 mpt2xopovel 6985 brtpos 7000 dftpos3 7009 erinxp 7455 qliftfun 7466 pw2f1olem 7694 infm3 10590 prime 11039 predfz 11941 hashf1lem2 12660 smueqlem 14543 vdwmc2 15008 acsfiel 15638 subsubc 15836 ismgmid 16585 eqger 16945 eqgid 16947 gaorber 17040 symgfix2 17135 psrbaglefi 18673 znleval 19202 bastop2 20087 elcls2 20167 maxlp 20240 restopn2 20270 restdis 20271 1stccn 20555 tx1cn 20701 tx2cn 20702 imasnopn 20782 imasncld 20783 imasncls 20784 idqtop 20798 tgqtop 20804 filuni 20978 uffix2 21017 cnflf 21095 isfcls 21102 fclsopn 21107 cnfcf 21135 ptcmplem2 21146 xmeter 21526 imasf1oxms 21582 prdsbl 21584 caucfil 22331 cfilucfil4 22367 shft2rab 22539 sca2rab 22543 mbfinf 22700 mbfinfOLD 22701 i1f1lem 22726 i1fres 22742 itg1climres 22751 mbfi1fseqlem4 22755 iblpos 22829 itgposval 22832 cnplimc 22921 ply1remlem 23192 plyremlem 23336 dvdsflsumcom 24196 fsumvma2 24221 vmasum 24223 logfac2 24224 chpchtsum 24226 logfaclbnd 24229 lgsquadlem1 24361 lgsquadlem2 24362 lgsquadlem3 24363 dchrisum0lem1 24433 colinearalg 25019 nbgrael 25233 nbgraeledg 25237 nbgraf1olem1 25248 2spot2iun2spont 25698 eupath2lem2 25785 eupath2 25787 frgraeu 25861 usgreg2spot 25874 pjpreeq 27132 elnlfn 27662 fimarab 28320 fmptcof2 28334 dfcnv2 28354 2ndpreima 28363 f1od2 28384 fpwrelmap 28393 iocinioc2 28436 nndiffz1 28441 indpi1 28917 1stmbfm 29155 2ndmbfm 29156 eulerpartlemgh 29284 bnj1171 29881 mrsubrn 30223 elfuns 30753 fneval 31079 topdifinfindis 31819 phpreu 31993 poimirlem23 32027 poimirlem26 32030 poimirlem27 32031 areacirclem5 32100 prter3 32518 islshpat 32654 lfl1dim 32758 glbconxN 33014 cdlemefrs29bpre0 34034 dib1dim 34804 dib1dim2 34807 diclspsn 34833 dihopelvalcpre 34887 dih1dimatlem 34968 mapdordlem1a 35273 hdmapoc 35573 rmydioph 35940 pw2f1ocnv 35963 funbrafv2b 38806 dfafn5a 38807 nbgrel 39574 nbusgreledg 39585 nbusgredgeu0 39606 umgr2v2enb1 39749 eupth2lem2 40131 eupth2lems 40150 |
Copyright terms: Public domain | W3C validator |