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 238 | . 2 ⊢ (𝜒 → 𝜓) |
4 | 3imtr3.3 | . 2 ⊢ (𝜓 ↔ 𝜃) | |
5 | 3, 4 | sylib 221 | 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: rb-ax1 1760 speimfwALT 1973 cbv1v 2336 cbv1 2401 hblem 2867 hblemg 2868 nfcriiOLD 2897 axrep1 5177 tfinds2 7639 smores 8086 idssen 8670 1sdom 8878 itunitc1 10031 dominf 10056 dominfac 10184 ssxr 10899 nnwos 12508 pmatcollpw3lem 21677 ppttop 21901 ptclsg 22509 sincosq3sgn 25387 adjbdln 30161 fmptdF 30710 funcnv4mpt 30723 disjdsct 30752 esumpcvgval 31755 esumcvg 31763 measiuns 31894 ballotlemodife 32173 bnj605 32597 bnj594 32602 acycgr0v 32820 prclisacycgr 32823 ssttrcl 33511 xpord3ind 33534 imagesset 33989 meran1 34334 meran3 34336 bj-modal4e 34631 f1omptsnlem 35241 mptsnunlem 35243 topdifinffinlem 35252 relowlpssretop 35269 poimirlem25 35537 eqelb 36117 symrefref3 36413 dedths 36711 sn-axrep5v 39905 dffltz 40172 mzpincl 40257 lerabdioph 40328 ltrabdioph 40331 nerabdioph 40332 dvdsrabdioph 40333 frege91 41237 frege97 41243 frege98 41244 frege109 41255 sumnnodd 42844 aiotaval 44257 rrx2linest 45759 |
Copyright terms: Public domain | W3C validator |