![]() |
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 610 | . . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜏))) |
4 | 3anim123d.3 | . . 3 ⊢ (𝜑 → (𝜂 → 𝜁)) | |
5 | 3, 4 | anim12d 610 | . 2 ⊢ (𝜑 → (((𝜓 ∧ 𝜃) ∧ 𝜂) → ((𝜒 ∧ 𝜏) ∧ 𝜁))) |
6 | df-3an 1090 | . 2 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ ((𝜓 ∧ 𝜃) ∧ 𝜂)) | |
7 | df-3an 1090 | . 2 ⊢ ((𝜒 ∧ 𝜏 ∧ 𝜁) ↔ ((𝜒 ∧ 𝜏) ∧ 𝜁)) | |
8 | 5, 6, 7 | 3imtr4g 296 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) → (𝜒 ∧ 𝜏 ∧ 𝜁))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∧ w3a 1088 |
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 df-an 398 df-3an 1090 |
This theorem is referenced by: pofun 5607 isopolem 7342 issmo2 8349 smores 8352 inawina 10685 gchina 10694 repswcshw 14762 coprmprod 16598 issubmnd 18652 issubg2 19021 issubrg2 20339 ocv2ss 21226 issubassa3 21420 sslm 22803 cmetcaulem 24805 axcontlem4 28225 axcontlem8 28229 redwlk 28929 clwwlknwwlksn 29291 numclwwlk1lem2foa 29607 dipsubdir 30101 subgrpth 34125 cgr3tr4 35024 idinside 35056 ftc1anclem7 36567 fzmul 36609 fdc1 36614 rngosubdi 36813 rngosubdir 36814 cdlemg33a 39577 upwlkwlk 46517 issubrng2 46737 rnglidlmsgrp 46757 rnglidlrng 46758 |
Copyright terms: Public domain | W3C validator |