| 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 239 | . 2 ⊢ (𝜑 → (𝜓 → 𝜏)) |
| 5 | 1, 4 | sylbird 260 | 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: tz6.12i 6934 f1imass 7284 focdmex 7980 tposfn2 8273 naddel1 8725 eroveu 8852 sdomel 9164 ackbij1lem16 10274 ltapr 11085 rpnnen1lem5 13023 qbtwnre 13241 om2uzlt2i 13992 m1dvdsndvds 16836 pcpremul 16881 pcaddlem 16926 pockthlem 16943 prmreclem6 16959 catidd 17723 issgrpd 18743 ghmf1 19264 gexdvds 19602 sylow1lem1 19616 lt6abl 19913 ablfacrplem 20085 isdomn4 20716 drnginvrn0 20754 issrngd 20856 islssd 20933 znrrg 21584 isphld 21672 cnllycmp 24988 nmhmcn 25153 minveclem7 25469 ioorcl2 25607 itg2seq 25777 dvlip2 26034 mdegmullem 26117 plyco0 26231 sincosq1sgn 26540 sincosq2sgn 26541 logcj 26648 argimgt0 26654 lgseisenlem2 27420 sleadd1im 28020 sleadd1 28022 sltonold 28283 om2noseqlt2 28306 remulscllem2 28433 eengtrkg 29001 eengtrkge 29002 ubthlem2 30890 minvecolem7 30902 nmcexi 32045 lnconi 32052 pjnormssi 32187 opsbc2ie 32495 qusvscpbl 33379 tan2h 37619 lindsadd 37620 itg2gt0cn 37682 divrngcl 37964 lshpcmp 38989 cdlemk35s 40939 cdlemk39s 40941 cdlemk42 40943 dihlspsnat 41335 clcnvlem 43636 tz6.12i-afv2 47255 sqrtnegnre 47319 |
| Copyright terms: Public domain | W3C validator |