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 282 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒)) |
4 | 3bitr3d.3 | . 2 ⊢ (𝜑 → (𝜒 ↔ 𝜏)) | |
5 | 3, 4 | bitrd 280 | 1 ⊢ (𝜑 → (𝜃 ↔ 𝜏)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 |
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 208 |
This theorem is referenced by: sbcne12 4361 fnprb 6962 fntpb 6963 eloprabga 7250 ordsucuniel 7528 ordsucun 7529 oeoa 8212 ereldm 8326 boxcutc 8493 mapen 8669 mapfien 8859 wemapwe 9148 sdom2en01 9712 prlem936 10457 subcan 10929 mulcan1g 11281 conjmul 11345 ltrec 11510 rebtwnz 12335 xposdif 12643 divelunit 12868 fseq1m1p1 12970 fzm1 12975 fllt 13164 hashfacen 13800 hashf1 13803 ccat0 13917 lenegsq 14668 dvdsmod 15666 bitsmod 15773 smueqlem 15827 rpexp 16052 eulerthlem2 16107 odzdvds 16120 pcelnn 16194 xpsle 16840 isepi 16998 fthmon 17185 pospropd 17732 grpidpropd 17860 mndpropd 17924 mhmpropd 17950 grppropd 18056 ghmnsgima 18320 mndodcong 18599 odf1 18618 odf1o1 18626 sylow3lem6 18686 lsmcntzr 18735 efgredlema 18795 cmnpropd 18845 dprdf11 19074 ringpropd 19261 dvdsrpropd 19375 abvpropd 19542 lmodprop2d 19625 lsspropd 19718 lmhmpropd 19774 lbspropd 19800 lvecvscan 19812 lvecvscan2 19813 assapropd 20029 chrnzr 20605 zndvds0 20625 ip2eq 20725 phlpropd 20727 qtopcn 22250 tsmsf1o 22680 xmetgt0 22895 txmetcnp 23084 metustsym 23092 nlmmul0or 23219 cnmet 23307 evth 23490 isclmp 23628 minveclem3b 23958 mbfposr 24180 itg2cn 24291 iblcnlem 24316 dvcvx 24544 ulm2 24900 efeq1 25040 dcubic 25351 mcubic 25352 dquart 25358 birthdaylem3 25458 ftalem2 25578 issqf 25640 sqff1o 25686 bposlem7 25793 lgsabs1 25839 gausslemma2dlem1a 25868 lgsquadlem2 25884 addsq2reu 25943 dchrisum0lem1 26019 opphllem6 26465 colhp 26483 lmiinv 26505 lmiopp 26515 wlkeq 27342 eupth2lem3lem3 27936 eupth2lem3lem6 27939 nmounbi 28480 ip2eqi 28560 hvmulcan 28776 hvsubcan2 28779 hi2eq 28809 fh2 29323 riesz4i 29767 cvbr4i 30071 xdivpnfrp 30536 isorng 30799 qusker 30845 ellspds 30860 ballotlemfc0 31649 ballotlemfcc 31650 sgnmulsgn 31706 sgnmulsgp 31707 subfacp1lem5 32328 eqfunresadj 32901 sltrec 33175 topfneec2 33601 neibastop3 33607 unccur 34756 cos2h 34764 tan2h 34765 poimirlem25 34798 poimirlem27 34800 dvasin 34859 caures 34916 ismtyima 34962 isdmn3 35233 dmecd 35443 releldmqscoss 35774 tendospcanN 38039 dochsncom 38398 or3or 40249 neicvgel1 40347 rusbcALT 40648 sbcoreleleqVD 41070 climreeq 41770 coseq0 42021 mgmhmpropd 43929 affinecomb1 44617 eenglngeehlnmlem1 44652 2sphere 44664 line2 44667 itscnhlc0yqe 44674 itscnhlc0xyqsol 44680 |
Copyright terms: Public domain | W3C validator |