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 291. 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 238 | . 2 ⊢ (𝜑 → (𝜓 → 𝜏)) |
5 | 1, 4 | sylbird 259 | 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: tz6.12i 6800 f1imass 7137 fornex 7798 tposfn2 8064 eroveu 8601 sdomel 8911 ackbij1lem16 9991 ltapr 10801 rpnnen1lem5 12721 qbtwnre 12933 om2uzlt2i 13671 m1dvdsndvds 16499 pcpremul 16544 pcaddlem 16589 pockthlem 16606 prmreclem6 16622 catidd 17389 ghmf1 18863 gexdvds 19189 sylow1lem1 19203 lt6abl 19496 ablfacrplem 19668 drnginvrn0 20009 issrngd 20121 islssd 20197 znrrg 20773 isphld 20859 cnllycmp 24119 nmhmcn 24283 minveclem7 24599 ioorcl2 24736 itg2seq 24907 dvlip2 25159 mdegmullem 25243 plyco0 25353 sincosq1sgn 25655 sincosq2sgn 25656 logcj 25761 argimgt0 25767 lgseisenlem2 26524 eengtrkg 27354 eengtrkge 27355 ubthlem2 29233 minvecolem7 29245 nmcexi 30388 lnconi 30395 pjnormssi 30530 opsbc2ie 30824 qusvscpbl 31551 naddel1 33839 tan2h 35769 lindsadd 35770 itg2gt0cn 35832 divrngcl 36115 lshpcmp 37002 cdlemk35s 38951 cdlemk39s 38953 cdlemk42 38955 dihlspsnat 39347 isdomn4 40172 clcnvlem 41231 tz6.12i-afv2 44735 sqrtnegnre 44799 |
Copyright terms: Public domain | W3C validator |