Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3imtr3d | Structured version Visualization version GIF version |
Description: More general version of 3imtr3i 294. Useful for converting conditional definitions in a formula. (Contributed by NM, 8-Apr-1996.) |
Ref | Expression |
---|---|
3imtr3d.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
3imtr3d.2 | ⊢ (𝜑 → (𝜓 ↔ 𝜃)) |
3imtr3d.3 | ⊢ (𝜑 → (𝜒 ↔ 𝜏)) |
Ref | Expression |
---|---|
3imtr3d | ⊢ (𝜑 → (𝜃 → 𝜏)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3imtr3d.2 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃)) | |
2 | 3imtr3d.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
3 | 3imtr3d.3 | . . 3 ⊢ (𝜑 → (𝜒 ↔ 𝜏)) | |
4 | 2, 3 | sylibd 242 | . 2 ⊢ (𝜑 → (𝜓 → 𝜏)) |
5 | 1, 4 | sylbird 263 | 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: tz6.12i 6700 f1imass 7033 fornex 7682 tposfn2 7943 eroveu 8423 sdomel 8714 ackbij1lem16 9735 ltapr 10545 rpnnen1lem5 12463 qbtwnre 12675 om2uzlt2i 13410 m1dvdsndvds 16235 pcpremul 16280 pcaddlem 16324 pockthlem 16341 prmreclem6 16357 catidd 17054 ghmf1 18505 gexdvds 18827 sylow1lem1 18841 lt6abl 19134 ablfacrplem 19306 drnginvrn0 19639 issrngd 19751 islssd 19826 znrrg 20384 isphld 20470 cnllycmp 23708 nmhmcn 23872 minveclem7 24187 ioorcl2 24324 itg2seq 24495 dvlip2 24747 mdegmullem 24831 plyco0 24941 sincosq1sgn 25243 sincosq2sgn 25244 logcj 25349 argimgt0 25355 lgseisenlem2 26112 eengtrkg 26932 eengtrkge 26933 ubthlem2 28806 minvecolem7 28818 nmcexi 29961 lnconi 29968 pjnormssi 30103 opsbc2ie 30398 qusvscpbl 31123 naddel1 33480 tan2h 35392 lindsadd 35393 itg2gt0cn 35455 divrngcl 35738 lshpcmp 36625 cdlemk35s 38574 cdlemk39s 38576 cdlemk42 38578 dihlspsnat 38970 isdomn4 39763 clcnvlem 40776 tz6.12i-afv2 44268 sqrtnegnre 44333 |
Copyright terms: Public domain | W3C validator |