![]() |
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 283. 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 231 | . 2 ⊢ (𝜑 → (𝜓 → 𝜏)) |
5 | 1, 4 | sylbird 252 | 1 ⊢ (𝜑 → (𝜃 → 𝜏)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 |
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 199 |
This theorem is referenced by: tz6.12i 6437 f1imass 6749 fornex 7370 tposfn2 7612 eroveu 8081 sdomel 8349 ackbij1lem16 9345 ltapr 10155 rpnnen1lem5 12065 qbtwnre 12279 om2uzlt2i 13005 m1dvdsndvds 15836 pcpremul 15881 pcaddlem 15925 pockthlem 15942 prmreclem6 15958 catidd 16655 ghmf1 18002 gexdvds 18312 sylow1lem1 18326 lt6abl 18611 ablfacrplem 18780 drnginvrn0 19083 issrngd 19179 islssd 19254 znrrg 20235 isphld 20323 cnllycmp 23083 nmhmcn 23247 minveclem7 23545 ioorcl2 23680 itg2seq 23850 dvlip2 24099 mdegmullem 24179 plyco0 24289 pilem3OLD 24549 sincosq1sgn 24592 sincosq2sgn 24593 logcj 24693 argimgt0 24699 lgseisenlem2 25453 eengtrkg 26222 eengtrkge 26223 ubthlem2 28252 minvecolem7 28264 nmcexi 29410 lnconi 29417 pjnormssi 29552 tan2h 33890 itg2gt0cn 33953 divrngcl 34243 lshpcmp 35009 cdlemk35s 36958 cdlemk39s 36960 cdlemk42 36962 dihlspsnat 37354 clcnvlem 38713 tz6.12i-afv2 42097 |
Copyright terms: Public domain | W3C validator |