| 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 276. (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 279 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃)) |
| 4 | 3 | bicomd 223 | 1 ⊢ (𝜑 → (𝜃 ↔ 𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 |
| 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 207 |
| This theorem is referenced by: 3bitrrd 306 3bitr2rd 308 pm5.18 381 ifptru 1075 sbequ12a 2254 elrnmpt1 5971 fndmdif 7062 weniso 7374 sbcopeq1a 8074 xpord2pred 8170 snmapen 9078 dmttrcl 9761 cfss 10305 posdif 11756 lesub1 11757 lesub0 11780 possumd 11888 ltdivmul 12143 ledivmul 12144 zlem1lt 12669 zltlem1 12670 negelrp 13068 ioon0 13413 fzn 13580 fzrev2 13628 fz1sbc 13640 elfzp1b 13641 sumsqeq0 14218 fz1isolem 14500 sqrtle 15299 absgt0 15363 isershft 15700 incexc2 15874 dvdssubr 16342 gcdn0gt0 16555 divgcdcoprmex 16703 pcfac 16937 ramval 17046 isrnghm 20441 iunocv 21699 ltbwe 22062 lmbrf 23268 perfcls 23373 ovolscalem1 25548 itg2mulclem 25781 sineq0 26566 efif1olem4 26587 logge0b 26673 loggt0b 26674 logle1b 26675 loglt1b 26676 atanord 26970 rlimcnp2 27009 bposlem7 27334 lgsprme0 27383 rpvmasum2 27556 sltsubsub2bd 28114 posdifsd 28127 sltmuldivwd 28226 trgcgrg 28523 legov3 28606 opphllem6 28760 ebtwntg 28997 wwlksm1edg 29901 clwlkclwwlk2 30022 hial2eq2 31126 adjsym 31852 cnvadj 31911 eigvalcl 31980 mddmd 32320 mdslmd2i 32349 elat2 32359 indpreima 32850 xdivpnfrp 32915 isorng 33329 ply1dg1rt 33604 unitdivcld 33900 ioosconn 35252 poimirlem26 37653 areacirclem1 37715 isat3 39308 ishlat3N 39355 cvrval5 39417 llnexchb2 39871 lhpoc2N 40017 lhprelat3N 40042 lautcnvle 40091 lautcvr 40094 ltrncnvatb 40140 cdlemb3 40608 cdlemg17h 40670 dih0vbN 41284 djhcvat42 41417 dvh4dimat 41440 mapdordlem2 41639 aks6d1c5lem1 42137 f1o2d2 42274 eluzp1 42341 reltsub1 42416 reltsubadd2 42417 sn-ltmul2d 42491 fsuppind 42600 diophun 42784 jm2.19lem4 43004 ordeldifsucon 43272 orddif0suc 43281 uneqsn 44038 xrralrecnnge 45401 limsupre2lem 45739 prprelb 47503 flsqrt5 47581 lincfsuppcl 48330 |
| Copyright terms: Public domain | W3C validator |