| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > 3anim123d | Structured version Visualization version GIF version | ||
| Description: Deduction joining 3 implications to form implication of conjunctions. (Contributed by NM, 24-Feb-2005.) |
| Ref | Expression |
|---|---|
| 3anim123d.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
| 3anim123d.2 | ⊢ (𝜑 → (𝜃 → 𝜏)) |
| 3anim123d.3 | ⊢ (𝜑 → (𝜂 → 𝜁)) |
| Ref | Expression |
|---|---|
| 3anim123d | ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) → (𝜒 ∧ 𝜏 ∧ 𝜁))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 3anim123d.1 | . . . 4 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
| 2 | 3anim123d.2 | . . . 4 ⊢ (𝜑 → (𝜃 → 𝜏)) | |
| 3 | 1, 2 | anim12d 609 | . . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜏))) |
| 4 | 3anim123d.3 | . . 3 ⊢ (𝜑 → (𝜂 → 𝜁)) | |
| 5 | 3, 4 | anim12d 609 | . 2 ⊢ (𝜑 → (((𝜓 ∧ 𝜃) ∧ 𝜂) → ((𝜒 ∧ 𝜏) ∧ 𝜁))) |
| 6 | df-3an 1089 | . 2 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ ((𝜓 ∧ 𝜃) ∧ 𝜂)) | |
| 7 | df-3an 1089 | . 2 ⊢ ((𝜒 ∧ 𝜏 ∧ 𝜁) ↔ ((𝜒 ∧ 𝜏) ∧ 𝜁)) | |
| 8 | 5, 6, 7 | 3imtr4g 296 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) → (𝜒 ∧ 𝜏 ∧ 𝜁))) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 |
| 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 df-an 396 df-3an 1089 |
| This theorem is referenced by: pofun 5610 isopolem 7365 issmo2 8389 smores 8392 inawina 10730 gchina 10739 repswcshw 14850 coprmprod 16698 issubmnd 18774 issubg2 19159 issubrng2 20558 issubrg2 20592 rnglidlmsgrp 21256 rnglidlrng 21257 ocv2ss 21691 issubassa3 21886 sslm 23307 cmetcaulem 25322 axcontlem4 28982 axcontlem8 28986 redwlk 29690 clwwlknwwlksn 30057 numclwwlk1lem2foa 30373 dipsubdir 30867 constrconj 33786 subgrpth 35139 cgr3tr4 36053 idinside 36085 ftc1anclem7 37706 fzmul 37748 fdc1 37753 rngosubdi 37952 rngosubdir 37953 cdlemg33a 40708 grtrimap 47915 grimgrtri 47916 grlimgrtri 47963 upwlkwlk 48055 |
| Copyright terms: Public domain | W3C validator |