![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > 3bitr3d | 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: -> wi 4 <-> wb 184 |
This theorem is referenced by: sbcne12 3827 sbcne12gOLD 3828 csbcomgOLD 3838 fnprb 6129 eloprabga 6389 ordsucuniel 6659 ordsucun 6660 oeoa 7265 ereldm 7374 boxcutc 7532 mapen 7701 mapfien 7887 mapfienOLD 8159 wemapwe 8160 wemapweOLD 8161 sdom2en01 8703 prlem936 9446 subcan 9897 mulcan1g 10227 conjmul 10286 ltrec 10451 rebtwnz 11210 xposdif 11483 infmxrgelb 11555 divelunit 11691 fseq1m1p1 11782 fzm1 11787 fllt 11943 hashfacen 12503 hashf1 12506 lenegsq 13153 dvdsmod 14043 bitsmod 14086 smueqlem 14140 rpexp 14261 eulerthlem2 14312 odzdvds 14322 pcelnn 14393 xpsle 14978 isepi 15135 fthmon 15296 pospropd 15764 grpidpropd 15888 mndpropd 15946 mhmpropd 15972 grppropd 16068 ghmnsgima 16290 mndodcong 16566 odf1 16584 odf1o1 16592 sylow3lem6 16652 lsmcntzr 16698 efgredlema 16758 cmnpropd 16807 dprdf11 17063 dprdf11OLD 17070 ringpropd 17230 dvdsrpropd 17345 abvpropd 17491 lmodprop2d 17572 lsspropd 17663 lmhmpropd 17719 lbspropd 17745 lvecvscan 17757 lvecvscan2 17758 assapropd 17976 chrnzr 18567 zndvds0 18589 ip2eq 18688 phlpropd 18690 qtopcn 20215 tsmsf1o 20647 xmetgt0 20861 txmetcnp 21050 metustsymOLD 21064 metustsym 21065 nlmmul0or 21192 cnmet 21279 evth 21459 minveclem3b 21843 mbfposr 22059 itg2cn 22170 iblcnlem 22195 dvcvx 22421 ulm2 22780 efeq1 22916 dcubic 23177 mcubic 23178 dquart 23184 birthdaylem3 23283 ftalem2 23347 issqf 23410 sqff1o 23456 bposlem7 23565 lgsabs1 23609 lgsquadlem2 23630 dchrisum0lem1 23701 opphllem6 24124 lmiinv 24158 cusgra2v 24462 eupath2lem3 24979 nmounbi 25691 ip2eqi 25772 hvmulcan 25989 hvsubcan2 25992 hi2eq 26022 fh2 26537 riesz4i 26982 cvbr4i 27286 xdivpnfrp 27629 isorng 27789 ballotlemfc0 28431 ballotlemfcc 28432 sgnmulsgn 28488 sgnmulsgp 28489 subfacp1lem5 28628 cos2h 30046 tan2h 30047 dvasin 30103 topfneec2 30174 neibastop3 30180 caures 30253 ismtyima 30299 isdmn3 30471 rusbcALT 31346 infrglb 31584 climreeq 31619 coseq0 31664 mgmhmpropd 32473 sbc3orgOLD 33303 tendospcanN 36750 dochsncom 37109 |
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 |
Copyright terms: Public domain | W3C validator |