![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > 3bitr3d | Structured version Unicode version |
Description: Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 24-Apr-1996.) |
Ref | Expression |
---|---|
3bitr3d.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3bitr3d.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3bitr3d.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3bitr3d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3bitr3d.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 3bitr3d.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | bitr3d 255 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3bitr3d.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | bitrd 253 |
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 185 |
This theorem is referenced by: sbcne12 3780 sbcne12gOLD 3781 csbcomgOLD 3791 fnprb 6038 eloprabga 6280 ordsucuniel 6538 ordsucun 6539 oeoa 7139 ereldm 7247 boxcutc 7409 mapen 7578 mapfien 7761 mapfienOLD 8031 wemapwe 8032 wemapweOLD 8033 sdom2en01 8575 prlem936 9320 subcan 9768 mulcan1g 10093 conjmul 10152 ltrec 10317 rebtwnz 11056 xposdif 11329 infmxrgelb 11401 divelunit 11537 fseq1m1p1 11645 fllt 11766 hashfacen 12318 hashf1 12321 lenegsq 12919 dvdsmod 13701 bitsmod 13743 smueqlem 13797 rpexp 13917 eulerthlem2 13968 odzdvds 13978 pcelnn 14047 xpsle 14630 isepi 14790 fthmon 14948 pospropd 15415 mndpropd 15557 grpidpropd 15558 mhmpropd 15581 grppropd 15667 ghmnsgima 15881 mndodcong 16158 odf1 16176 odf1o1 16184 sylow3lem6 16244 lsmcntzr 16290 efgredlema 16350 cmnpropd 16399 dprdf11 16627 dprdf11OLD 16634 rngpropd 16791 dvdsrpropd 16903 abvpropd 17042 lmodprop2d 17122 lsspropd 17213 lmhmpropd 17269 lbspropd 17295 lvecvscan 17307 lvecvscan2 17308 assapropd 17513 chrnzr 18079 zndvds0 18101 ip2eq 18200 phlpropd 18202 qtopcn 19412 tsmsf1o 19844 xmetgt0 20058 txmetcnp 20247 metustsymOLD 20261 metustsym 20262 nlmmul0or 20389 cnmet 20476 evth 20656 minveclem3b 21040 mbfposr 21256 itg2cn 21367 iblcnlem 21392 dvcvx 21618 ulm2 21976 efeq1 22111 dcubic 22367 mcubic 22368 dquart 22374 birthdaylem3 22473 ftalem2 22537 issqf 22600 sqff1o 22646 bposlem7 22755 lgsabs1 22799 lgsquadlem2 22820 dchrisum0lem1 22891 cusgra2v 23515 eupath2lem3 23745 nmounbi 24321 ip2eqi 24402 hvmulcan 24619 hvsubcan2 24622 hi2eq 24652 fh2 25167 riesz4i 25612 cvbr4i 25916 xdivpnfrp 26246 isorng 26405 ballotlemfc0 27012 ballotlemfcc 27013 sgnmulsgn 27069 sgnmulsgp 27070 subfacp1lem5 27209 cos2h 28564 tan2h 28565 dvasin 28621 topfneec2 28705 neibastop3 28724 caures 28797 ismtyima 28843 isdmn3 29015 rusbcALT 29834 infrglb 29912 climreeq 29927 sbc3orgOLD 31541 tendospcanN 34977 dochsncom 35336 |
Copyright terms: Public domain | W3C validator |