Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3imtr3i | Structured version Visualization version GIF version |
Description: A mixed syllogism inference, useful for removing a definition from both sides of an implication. (Contributed by NM, 10-Aug-1994.) |
Ref | Expression |
---|---|
3imtr3.1 | ⊢ (𝜑 → 𝜓) |
3imtr3.2 | ⊢ (𝜑 ↔ 𝜒) |
3imtr3.3 | ⊢ (𝜓 ↔ 𝜃) |
Ref | Expression |
---|---|
3imtr3i | ⊢ (𝜒 → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3imtr3.2 | . . 3 ⊢ (𝜑 ↔ 𝜒) | |
2 | 3imtr3.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
3 | 1, 2 | sylbir 237 | . 2 ⊢ (𝜒 → 𝜓) |
4 | 3imtr3.3 | . 2 ⊢ (𝜓 ↔ 𝜃) | |
5 | 3, 4 | sylib 220 | 1 ⊢ (𝜒 → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 |
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 209 |
This theorem is referenced by: rb-ax1 1753 speimfwALT 1967 cbv1v 2356 cbv1 2422 hblem 2943 hblemg 2944 nfcrii 2970 axrep1 5191 tfinds2 7578 smores 7989 idssen 8554 1sdom 8721 itunitc1 9842 dominf 9867 dominfac 9995 ssxr 10710 nnwos 12316 pmatcollpw3lem 21391 ppttop 21615 ptclsg 22223 sincosq3sgn 25086 adjbdln 29860 fmptdF 30401 funcnv4mpt 30414 disjdsct 30438 esumpcvgval 31337 esumcvg 31345 measiuns 31476 ballotlemodife 31755 bnj605 32179 bnj594 32184 acycgr0v 32395 prclisacycgr 32398 imagesset 33414 meran1 33759 meran3 33761 bj-modal4e 34049 f1omptsnlem 34620 mptsnunlem 34622 topdifinffinlem 34631 relowlpssretop 34648 poimirlem25 34932 eqelb 35517 symrefref3 35815 dedths 36113 sn-axrep5v 39128 dffltz 39291 mzpincl 39351 lerabdioph 39422 ltrabdioph 39425 nerabdioph 39426 dvdsrabdioph 39427 frege91 40320 frege97 40326 frege98 40327 frege109 40338 sumnnodd 41931 aiotaval 43313 rrx2linest 44749 |
Copyright terms: Public domain | W3C validator |