Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > bitr2d | Structured version Visualization version GIF version |
Description: Deduction form of bitr2i 277. (Contributed by NM, 9-Jun-2004.) |
Ref | Expression |
---|---|
bitr2d.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
bitr2d.2 | ⊢ (𝜑 → (𝜒 ↔ 𝜃)) |
Ref | Expression |
---|---|
bitr2d | ⊢ (𝜑 → (𝜃 ↔ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bitr2d.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | bitr2d.2 | . . 3 ⊢ (𝜑 → (𝜒 ↔ 𝜃)) | |
3 | 1, 2 | bitrd 280 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃)) |
4 | 3 | bicomd 224 | 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: 3bitrrd 307 3bitr2rd 309 pm5.18 383 ifptru 1065 sbequ12a 2246 elrnmpt1 5823 fndmdif 6804 weniso 7096 sbcopeq1a 7737 snmapen 8578 cfss 9675 posdif 11121 lesub1 11122 lesub0 11145 possumd 11253 ltdivmul 11503 ledivmul 11504 zlem1lt 12022 zltlem1 12023 negelrp 12410 ioon0 12752 fzn 12911 fzrev2 12959 fz1sbc 12971 elfzp1b 12972 sumsqeq0 13530 fz1isolem 13807 sqrtle 14608 absgt0 14672 isershft 15008 incexc2 15181 dvdssubr 15643 gcdn0gt0 15854 divgcdcoprmex 15998 pcfac 16223 ramval 16332 ltbwe 20181 mhpinvcl 20267 iunocv 20753 lmbrf 21796 perfcls 21901 ovolscalem1 24041 itg2mulclem 24274 sineq0 25036 efif1olem4 25056 logge0b 25141 loggt0b 25142 logle1b 25143 loglt1b 25144 atanord 25432 rlimcnp2 25471 bposlem7 25793 lgsprme0 25842 rpvmasum2 26015 trgcgrg 26228 legov3 26311 opphllem6 26465 ebtwntg 26695 wwlksm1edg 27586 clwlkclwwlk2 27708 hial2eq2 28811 adjsym 29537 cnvadj 29596 eigvalcl 29665 mddmd 30005 mdslmd2i 30034 elat2 30044 xdivpnfrp 30536 isorng 30799 unitdivcld 31043 indpreima 31183 ioosconn 32391 pdivsq 32878 poimirlem26 34799 areacirclem1 34863 isat3 36323 ishlat3N 36370 cvrval5 36431 llnexchb2 36885 lhpoc2N 37031 lhprelat3N 37056 lautcnvle 37105 lautcvr 37108 ltrncnvatb 37154 cdlemb3 37622 cdlemg17h 37684 dih0vbN 38298 djhcvat42 38431 dvh4dimat 38454 mapdordlem2 38653 reltsub1 39094 reltsubadd2 39095 diophun 39248 jm2.19lem4 39467 uneqsn 40251 xrralrecnnge 41538 limsupre2lem 41881 prprelb 43555 flsqrt5 43634 isrnghm 44091 lincfsuppcl 44396 |
Copyright terms: Public domain | W3C validator |