![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3bitr4rd | Structured version Visualization version GIF version |
Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.) |
Ref | Expression |
---|---|
3bitr4d.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
3bitr4d.2 | ⊢ (𝜑 → (𝜃 ↔ 𝜓)) |
3bitr4d.3 | ⊢ (𝜑 → (𝜏 ↔ 𝜒)) |
Ref | Expression |
---|---|
3bitr4rd | ⊢ (𝜑 → (𝜏 ↔ 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3bitr4d.3 | . . 3 ⊢ (𝜑 → (𝜏 ↔ 𝜒)) | |
2 | 3bitr4d.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | bitr4d 283 | . 2 ⊢ (𝜑 → (𝜏 ↔ 𝜓)) |
4 | 3bitr4d.2 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜓)) | |
5 | 3, 4 | bitr4d 283 | 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: snssg 4630 inimasn 5896 isof1oidb 6947 oacan 8031 ecdmn0 8193 wemapwe 9013 r1pw 9127 adderpqlem 10229 mulerpqlem 10230 lterpq 10245 ltanq 10246 genpass 10284 readdcan 10667 lemuldiv 11374 msq11 11395 avglt2 11730 qbtwnre 12446 iooshf 12669 clim2c 14700 lo1o1 14727 climabs0 14780 reef11 15309 absefib 15388 efieq1re 15389 nndivides 15454 oddnn02np1 15534 oddge22np1 15535 evennn02n 15536 evennn2n 15537 halfleoddlt 15548 pc2dvds 16048 pcmpt 16061 subsubc 16956 odmulgid 18415 gexdvds 18443 submcmn2 18688 obslbs 20560 cnntr 21571 cndis 21587 cnindis 21588 cnpdis 21589 lmres 21596 cmpfi 21704 ist0-4 22025 txhmeo 22099 tsmssubm 22438 blin 22718 cncfmet 23203 icopnfcnv 23233 lmmbrf 23552 iscauf 23570 causs 23588 mbfposr 23940 itg2gt0 24048 limcflf 24166 limcres 24171 lhop1 24298 dvdsr1p 24442 fsumvma2 25476 vmasum 25478 chpchtsum 25481 bposlem1 25546 iscgrgd 25985 tgcgr4 26003 lnrot1 26095 eqeelen 26377 nbusgreledg 26822 nb3grprlem2 26850 wspthsnwspthsnon 27381 rusgrnumwwlks 27439 clwlkclwwlk2 27467 clwwlkwwlksb 27519 clwwlknwwlksnb 27520 clwwlknonwwlknonb 27571 dmdmd 29764 nfpconfp 30063 funcnvmpt 30098 1stpreimas 30125 xrdifh 30187 ismntop 30880 eulerpartlemgh 31249 signslema 31445 fmlafvel 32242 topdifinfindis 34179 leceifl 34433 lindsadd 34437 lindsenlbs 34439 iblabsnclem 34507 ftc1anclem6 34524 areacirclem5 34538 areacirc 34539 brcoss3 35230 lsatfixedN 35697 cdlemg10c 37327 diaglbN 37743 dih1 37974 dihglbcpreN 37988 mapdcv 38348 ellz1 38870 islssfg 39176 proot1ex 39307 eliooshift 41345 clim2cf 41494 dfatdmfcoafv2 42991 sfprmdvdsmersenne 43272 odd2np1ALTV 43343 rrx2plordisom 44213 |
Copyright terms: Public domain | W3C validator |