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 265. (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 268 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃)) |
4 | 3 | bicomd 213 | 1 ⊢ (𝜑 → (𝜃 ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 |
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 197 |
This theorem is referenced by: 3bitrrd 295 3bitr2rd 297 pm5.18 371 ifptru 1023 sbequ12a 2113 elrnmpt1 5374 fndmdif 6321 weniso 6604 sbcopeq1a 7220 cfss 9087 posdif 10521 lesub1 10522 lesub0 10545 possumd 10652 ltdivmul 10898 ledivmul 10899 zlem1lt 11429 zltlem1 11430 negelrp 11864 ioon0 12201 fzn 12357 fzrev2 12404 fz1sbc 12416 elfzp1b 12417 sumsqeq0 12942 fz1isolem 13245 sqrtle 14001 absgt0 14064 isershft 14394 incexc2 14570 dvdssubr 15027 gcdn0gt0 15239 divgcdcoprmex 15380 pcfac 15603 ramval 15712 ltbwe 19472 iunocv 20025 lmbrf 21064 perfcls 21169 ovolscalem1 23281 itg2mulclem 23513 sineq0 24273 efif1olem4 24291 logge0b 24377 loggt0b 24378 logle1b 24379 loglt1b 24380 atanord 24654 rlimcnp2 24693 bposlem7 25015 lgsprme0 25064 rpvmasum2 25201 trgcgrg 25410 legov3 25493 opphllem6 25644 ebtwntg 25862 wwlksm1edg 26767 hial2eq2 27964 adjsym 28692 cnvadj 28751 eigvalcl 28820 mddmd 29160 mdslmd2i 29189 elat2 29199 xdivpnfrp 29641 isorng 29799 unitdivcld 29947 indpreima 30087 ioosconn 31229 pdivsq 31635 poimirlem26 33435 areacirclem1 33500 isat3 34594 ishlat3N 34641 cvrval5 34701 llnexchb2 35155 lhpoc2N 35301 lhprelat3N 35326 lautcnvle 35375 lautcvr 35378 ltrncnvatb 35424 cdlemb3 35894 cdlemg17h 35956 dih0vbN 36571 djhcvat42 36704 dvh4dimat 36727 mapdordlem2 36926 diophun 37337 jm2.19lem4 37559 uneqsn 38321 xrralrecnnge 39613 limsupre2lem 39956 flsqrt5 41509 isrnghm 41892 lincfsuppcl 42202 |
Copyright terms: Public domain | W3C validator |