Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > bitr3di | Structured version Visualization version GIF version |
Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.) |
Ref | Expression |
---|---|
bitr3di.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
bitr3di.2 | ⊢ (𝜓 ↔ 𝜃) |
Ref | Expression |
---|---|
bitr3di | ⊢ (𝜑 → (𝜒 ↔ 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bitr3di.2 | . . 3 ⊢ (𝜓 ↔ 𝜃) | |
2 | 1 | bicomi 227 | . 2 ⊢ (𝜃 ↔ 𝜓) |
3 | bitr3di.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
4 | 2, 3 | bitr2id 287 | 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: sbco3 2516 necon2bbid 2984 notzfaus 5254 fressnfv 6975 eluniima 7063 dfac2b 9744 alephval2 10186 adderpqlem 10568 1idpr 10643 leloe 10919 negeq0 11132 addeq0 11255 muleqadd 11476 addltmul 12066 xrleloe 12734 fzrev 13175 mod0 13449 modirr 13515 cjne0 14726 lenegsq 14884 fsumsplit 15305 sumsplit 15332 dvdsabseq 15874 xpsfrnel 17067 isacs2 17156 acsfn 17162 comfeq 17209 sgrp2nmndlem3 18352 resscntz 18726 gexdvds 18973 hauscmplem 22303 hausdiag 22542 utop3cls 23149 affineequivne 25710 ltgov 26688 ax5seglem4 27023 mdsl2i 30403 rspc2daf 30535 cycpmco2 31119 pl1cn 31619 fineqvpow 32778 satefvfmla1 33100 eqscut2 33737 topdifinfeq 35258 finxpreclem6 35304 ftc1anclem5 35591 fdc1 35641 relcnveq 36194 relcnveq2 36195 elrelscnveq 36347 elrelscnveq2 36348 lcvexchlem1 36785 lkreqN 36921 glbconxN 37129 islpln5 37286 islvol5 37330 cdlemefrs29bpre0 38147 cdlemg17h 38419 cdlemg33b 38458 brnonrel 40873 frege92 41240 e2ebind 41856 stoweidlem28 43244 |
Copyright terms: Public domain | W3C validator |