![]() |
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 234 | . 2 ⊢ (𝜒 → 𝜓) |
4 | 3imtr3.3 | . 2 ⊢ (𝜓 ↔ 𝜃) | |
5 | 3, 4 | sylib 217 | 1 ⊢ (𝜒 → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 |
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 206 |
This theorem is referenced by: rb-ax1 1754 speimfwALT 1968 cbv1v 2332 cbv1 2400 hblem 2869 hblemg 2870 nfcriiOLD 2899 sbhypf 3506 axrep1 5242 tfinds2 7797 smores 8295 idssen 8934 1sdomOLD 9190 ssttrcl 9648 itunitc1 10353 dominf 10378 dominfac 10506 ssxr 11221 nnwos 12837 pmatcollpw3lem 22128 ppttop 22353 ptclsg 22962 sincosq3sgn 25853 adjbdln 30923 fmptdF 31470 funcnv4mpt 31483 disjdsct 31512 esumpcvgval 32568 esumcvg 32576 measiuns 32707 ballotlemodife 32988 bnj605 33410 bnj594 33415 acycgr0v 33633 prclisacycgr 33636 imagesset 34527 meran1 34872 meran3 34874 bj-modal4e 35169 f1omptsnlem 35796 mptsnunlem 35798 topdifinffinlem 35807 relowlpssretop 35824 poimirlem25 36092 eqbrb 36679 eqelb 36681 symrefref3 37015 dedths 37413 sn-axrep5v 40626 dffltz 40948 mzpincl 41033 lerabdioph 41104 ltrabdioph 41107 nerabdioph 41108 dvdsrabdioph 41109 finona1cl 41705 frege91 42206 frege97 42212 frege98 42213 frege109 42224 sumnnodd 43841 aiotaval 45297 rrx2linest 46798 |
Copyright terms: Public domain | W3C validator |