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 4363 fnprb 6963 fntpb 6964 eloprabga 7250 ordsucuniel 7527 ordsucun 7528 oeoa 8213 ereldm 8327 boxcutc 8494 mapen 8670 mapfien 8860 wemapwe 9149 sdom2en01 9713 prlem936 10458 subcan 10930 mulcan1g 11282 conjmul 11346 ltrec 11511 rebtwnz 12336 xposdif 12645 divelunit 12870 fseq1m1p1 12972 fzm1 12977 fllt 13166 hashfacen 13802 hashf1 13805 ccat0 13919 lenegsq 14670 dvdsmod 15668 bitsmod 15775 smueqlem 15829 rpexp 16054 eulerthlem2 16109 odzdvds 16122 pcelnn 16196 xpsle 16842 isepi 17000 fthmon 17187 pospropd 17734 grpidpropd 17862 mndpropd 17926 mhmpropd 17952 grppropd 18058 ghmnsgima 18322 mndodcong 18601 odf1 18620 odf1o1 18628 sylow3lem6 18688 lsmcntzr 18737 efgredlema 18797 cmnpropd 18847 dprdf11 19076 ringpropd 19263 dvdsrpropd 19377 abvpropd 19544 lmodprop2d 19627 lsspropd 19720 lmhmpropd 19776 lbspropd 19802 lvecvscan 19814 lvecvscan2 19815 assapropd 20031 chrnzr 20607 zndvds0 20627 ip2eq 20727 phlpropd 20729 qtopcn 22252 tsmsf1o 22682 xmetgt0 22897 txmetcnp 23086 metustsym 23094 nlmmul0or 23221 cnmet 23309 evth 23492 isclmp 23630 minveclem3b 23960 mbfposr 24182 itg2cn 24293 iblcnlem 24318 dvcvx 24546 ulm2 24902 efeq1 25040 dcubic 25351 mcubic 25352 dquart 25358 birthdaylem3 25459 ftalem2 25579 issqf 25641 sqff1o 25687 bposlem7 25794 lgsabs1 25840 gausslemma2dlem1a 25869 lgsquadlem2 25885 addsq2reu 25944 dchrisum0lem1 26020 opphllem6 26466 colhp 26484 lmiinv 26506 lmiopp 26516 wlkeq 27343 eupth2lem3lem3 27937 eupth2lem3lem6 27940 nmounbi 28481 ip2eqi 28561 hvmulcan 28777 hvsubcan2 28780 hi2eq 28810 fh2 29324 riesz4i 29768 cvbr4i 30072 xdivpnfrp 30537 isorng 30800 qusker 30846 ellspds 30861 ballotlemfc0 31650 ballotlemfcc 31651 sgnmulsgn 31707 sgnmulsgp 31708 subfacp1lem5 32329 eqfunresadj 32902 sltrec 33176 topfneec2 33602 neibastop3 33608 unccur 34757 cos2h 34765 tan2h 34766 poimirlem25 34799 poimirlem27 34801 dvasin 34860 caures 34918 ismtyima 34964 isdmn3 35235 dmecd 35445 releldmqscoss 35776 tendospcanN 38041 dochsncom 38400 or3or 40251 neicvgel1 40349 rusbcALT 40651 sbcoreleleqVD 41073 climreeq 41774 coseq0 42025 mgmhmpropd 43899 affinecomb1 44587 eenglngeehlnmlem1 44622 2sphere 44634 line2 44637 itscnhlc0yqe 44644 itscnhlc0xyqsol 44650 |
Copyright terms: Public domain | W3C validator |