Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3bitr3d | Structured version Visualization 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 270 | . 2 |
4 | 3bitr3d.3 | . 2 | |
5 | 3, 4 | bitrd 268 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 196 |
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 197 |
This theorem is referenced by: sbcne12 3986 fnprb 6472 fntpb 6473 eloprabga 6747 ordsucuniel 7024 ordsucun 7025 oeoa 7677 ereldm 7790 boxcutc 7951 mapen 8124 mapfien 8313 wemapwe 8594 sdom2en01 9124 prlem936 9869 subcan 10336 mulcan1g 10680 conjmul 10742 ltrec 10905 rebtwnz 11787 xposdif 12092 divelunit 12314 fseq1m1p1 12415 fzm1 12420 fllt 12607 hashfacen 13238 hashf1 13241 lenegsq 14060 dvdsmod 15050 bitsmod 15158 smueqlem 15212 rpexp 15432 eulerthlem2 15487 odzdvds 15500 pcelnn 15574 xpsle 16241 isepi 16400 fthmon 16587 pospropd 17134 grpidpropd 17261 mndpropd 17316 mhmpropd 17341 grppropd 17437 ghmnsgima 17684 mndodcong 17961 odf1 17979 odf1o1 17987 sylow3lem6 18047 lsmcntzr 18093 efgredlema 18153 cmnpropd 18202 dprdf11 18422 ringpropd 18582 dvdsrpropd 18696 abvpropd 18842 lmodprop2d 18925 lsspropd 19017 lmhmpropd 19073 lbspropd 19099 lvecvscan 19111 lvecvscan2 19112 assapropd 19327 chrnzr 19878 zndvds0 19899 ip2eq 19998 phlpropd 20000 qtopcn 21517 tsmsf1o 21948 xmetgt0 22163 txmetcnp 22352 metustsym 22360 nlmmul0or 22487 cnmet 22575 evth 22758 isclmp 22897 minveclem3b 23199 mbfposr 23419 itg2cn 23530 iblcnlem 23555 dvcvx 23783 ulm2 24139 efeq1 24275 dcubic 24573 mcubic 24574 dquart 24580 birthdaylem3 24680 ftalem2 24800 issqf 24862 sqff1o 24908 bposlem7 25015 lgsabs1 25061 gausslemma2dlem1a 25090 lgsquadlem2 25106 dchrisum0lem1 25205 opphllem6 25644 colhp 25662 lmiinv 25684 lmiopp 25694 eupth2lem3lem3 27090 eupth2lem3lem6 27093 nmounbi 27631 ip2eqi 27712 hvmulcan 27929 hvsubcan2 27932 hi2eq 27962 fh2 28478 riesz4i 28922 cvbr4i 29226 xdivpnfrp 29641 isorng 29799 ballotlemfc0 30554 ballotlemfcc 30555 sgnmulsgn 30611 sgnmulsgp 30612 subfacp1lem5 31166 eqfunresadj 31659 sltrec 31924 topfneec2 32351 neibastop3 32357 unccur 33392 cos2h 33400 tan2h 33401 poimirlem25 33434 poimirlem27 33436 dvasin 33496 caures 33556 ismtyima 33602 isdmn3 33873 dmecd 34074 tendospcanN 36312 dochsncom 36671 or3or 38319 neicvgel1 38417 rusbcALT 38640 sbc3orgOLD 38742 climreeq 39845 coseq0 40075 mgmhmpropd 41785 |
Copyright terms: Public domain | W3C validator |