![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3bitr3d | Structured version Visualization version GIF 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 281 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒)) |
4 | 3bitr3d.3 | . 2 ⊢ (𝜑 → (𝜒 ↔ 𝜏)) | |
5 | 3, 4 | bitrd 279 | 1 ⊢ (𝜑 → (𝜃 ↔ 𝜏)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 |
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 206 |
This theorem is referenced by: sbcne12 4411 fnprb 7205 fntpb 7206 eqfunresadj 7352 eloprabga 7511 eloprabgaOLD 7512 ordsucuniel 7807 ordsucun 7808 oeoa 8593 ereldm 8747 boxcutc 8931 mapen 9137 mapfien 9399 wemapwe 9688 sdom2en01 10293 prlem936 11038 subcan 11511 mulcan1g 11863 conjmul 11927 ltrec 12092 rebtwnz 12927 xposdif 13237 divelunit 13467 fseq1m1p1 13572 fzm1 13577 fllt 13767 hashfacen 14409 hashfacenOLD 14410 hashf1 14414 ccat0 14522 lenegsq 15263 dvdsmod 16268 bitsmod 16373 smueqlem 16427 rpexp 16655 eulerthlem2 16711 odzdvds 16724 pcelnn 16799 xpsle 17521 isepi 17683 fthmon 17874 cat1 18043 pospropd 18276 grpidpropd 18577 sgrppropd 18618 mndpropd 18646 mhmpropd 18674 grppropd 18833 ghmnsgima 19110 mndodcong 19403 odf1 19423 odf1o1 19433 sylow3lem6 19493 lsmcntzr 19541 efgredlema 19601 cmnpropd 19652 qusecsub 19695 dprdf11 19885 ringpropd 20092 dvdsrpropd 20219 resrhm2b 20382 abvpropd 20438 lmodprop2d 20522 lsspropd 20616 lmhmpropd 20672 lbspropd 20698 lvecvscan 20712 lvecvscan2 20713 chrnzr 21066 zndvds0 21090 ip2eq 21190 phlpropd 21192 assapropd 21408 qtopcn 23200 tsmsf1o 23631 xmetgt0 23846 txmetcnp 24038 metustsym 24046 nlmmul0or 24182 cnmet 24270 evth 24457 isclmp 24595 minveclem3b 24927 mbfposr 25151 itg2cn 25263 iblcnlem 25288 dvcvx 25519 ulm2 25879 efeq1 26019 dcubic 26331 mcubic 26332 dquart 26338 birthdaylem3 26438 ftalem2 26558 issqf 26620 sqff1o 26666 bposlem7 26773 lgsabs1 26819 gausslemma2dlem1a 26848 lgsquadlem2 26864 addsq2reu 26923 dchrisum0lem1 26999 sltrec 27301 opphllem6 27983 colhp 28001 lmiinv 28023 lmiopp 28033 wlkeq 28871 eupth2lem3lem3 29463 eupth2lem3lem6 29466 nmounbi 30007 ip2eqi 30087 hvmulcan 30303 hvsubcan2 30306 hi2eq 30336 fh2 30850 riesz4i 31294 cvbr4i 31598 xdivpnfrp 32077 isorng 32386 qusker 32433 ellspds 32450 ply1moneq 32612 ballotlemfc0 33429 ballotlemfcc 33430 sgnmulsgn 33486 sgnmulsgp 33487 subfacp1lem5 34113 topfneec2 35179 neibastop3 35185 unccur 36409 cos2h 36417 tan2h 36418 poimirlem25 36451 poimirlem27 36453 dvasin 36510 caures 36566 ismtyima 36609 isdmn3 36880 dmecd 37111 releldmqscoss 37468 tendospcanN 39832 dochsncom 40191 f1o2d2 41004 sqrtcval 42325 or3or 42707 neicvgel1 42803 rusbcALT 43131 sbcoreleleqVD 43553 climreeq 44264 coseq0 44515 mgmhmpropd 46490 rngpropd 46608 affinecomb1 47290 eenglngeehlnmlem1 47325 2sphere 47337 line2 47340 itscnhlc0yqe 47347 itscnhlc0xyqsol 47353 |
Copyright terms: Public domain | W3C validator |