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 285 | . 2 ⊢ (𝜑 → (𝜏 ↔ 𝜓)) |
4 | 3bitr4d.2 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜓)) | |
5 | 3, 4 | bitr4d 285 | 1 ⊢ (𝜑 → (𝜏 ↔ 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 |
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 210 |
This theorem is referenced by: snssg 4695 inimasn 6016 isof1oidb 7130 oacan 8273 ecdmn0 8435 wemapwe 9309 r1pw 9458 adderpqlem 10565 mulerpqlem 10566 lterpq 10581 ltanq 10582 genpass 10620 readdcan 11003 lemuldiv 11709 msq11 11730 avglt2 12066 qbtwnre 12786 iooshf 13011 clim2c 15063 lo1o1 15090 climabs0 15143 reef11 15677 absefib 15756 efieq1re 15757 nndivides 15822 oddnn02np1 15906 oddge22np1 15907 evennn02n 15908 evennn2n 15909 halfleoddlt 15920 pc2dvds 16429 pcmpt 16442 subsubc 17356 odmulgid 18942 gexdvds 18970 submcmn2 19221 obslbs 20689 cnntr 22169 cndis 22185 cnindis 22186 cnpdis 22187 lmres 22194 cmpfi 22302 ist0-4 22623 txhmeo 22697 tsmssubm 23037 blin 23316 cncfmet 23803 icopnfcnv 23836 lmmbrf 24156 iscauf 24174 causs 24192 mbfposr 24546 itg2gt0 24655 limcflf 24775 limcres 24780 lhop1 24908 dvdsr1p 25056 fsumvma2 26092 vmasum 26094 chpchtsum 26097 bposlem1 26162 iscgrgd 26601 tgcgr4 26619 lnrot1 26711 eqeelen 26992 nbusgreledg 27438 nb3grprlem2 27466 wspthsnwspthsnon 27997 rusgrnumwwlks 28055 clwwlkwwlksb 28134 clwwlknwwlksnb 28135 dmdmd 30378 nfpconfp 30683 funcnvmpt 30721 1stpreimas 30755 xrdifh 30818 swrdrn3 30944 lsmsnorb 31290 rhmpreimacnlem 31545 ismntop 31685 eulerpartlemgh 32054 signslema 32250 fmlafvel 33057 topdifinfindis 35251 leceifl 35501 lindsadd 35505 lindsenlbs 35507 iblabsnclem 35575 ftc1anclem6 35590 areacirclem5 35604 areacirc 35605 brcoss3 36291 lsatfixedN 36758 cdlemg10c 38388 diaglbN 38804 dih1 39035 dihglbcpreN 39049 mapdcv 39409 dvdsexpnn0 40047 ellz1 40290 islssfg 40596 proot1ex 40727 eliooshift 42717 clim2cf 42864 dfatdmfcoafv2 44416 sfprmdvdsmersenne 44726 odd2np1ALTV 44797 rrx2plordisom 45740 i0oii 45884 io1ii 45885 |
Copyright terms: Public domain | W3C validator |