|   | 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 235 | . 2 ⊢ (𝜒 → 𝜓) | 
| 4 | 3imtr3.3 | . 2 ⊢ (𝜓 ↔ 𝜃) | |
| 5 | 3, 4 | sylib 218 | 1 ⊢ (𝜒 → 𝜃) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 | 
| 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 207 | 
| This theorem is referenced by: rb-ax1 1751 speimfwALT 1963 cbv1v 2337 cbv1 2406 hblem 2872 hblemg 2873 sbhypf 3543 axrep1 5279 axrep4v 5283 axrep4 5284 tfinds2 7886 smores 8393 idssen 9038 1sdomOLD 9286 ssttrcl 9756 itunitc1 10461 dominf 10486 dominfac 10614 ssxr 11331 nnwos 12958 pmatcollpw3lem 22790 ppttop 23015 ptclsg 23624 sincosq3sgn 26543 adjbdln 32103 fmptdF 32667 funcnv4mpt 32680 disjdsct 32713 esumpcvgval 34080 esumcvg 34088 measiuns 34219 ballotlemodife 34501 bnj605 34922 bnj594 34927 acycgr0v 35154 prclisacycgr 35157 imagesset 35955 meran1 36413 meran3 36415 bj-modal4e 36717 f1omptsnlem 37338 mptsnunlem 37340 topdifinffinlem 37349 relowlpssretop 37366 poimirlem25 37653 eqbrb 38235 eqelb 38237 symrefref3 38566 dedths 38964 sn-axrep5v 42256 dffltz 42649 mzpincl 42750 lerabdioph 42821 ltrabdioph 42824 nerabdioph 42825 dvdsrabdioph 42826 finona1cl 43471 frege91 43972 frege97 43978 frege98 43979 frege109 43990 sumnnodd 45650 limsupvaluz2 45758 aiotaval 47112 rrx2linest 48668 fonex 48774 | 
| Copyright terms: Public domain | W3C validator |