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 608 | . . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜏))) |
4 | 3anim123d.3 | . . 3 ⊢ (𝜑 → (𝜂 → 𝜁)) | |
5 | 3, 4 | anim12d 608 | . 2 ⊢ (𝜑 → (((𝜓 ∧ 𝜃) ∧ 𝜂) → ((𝜒 ∧ 𝜏) ∧ 𝜁))) |
6 | df-3an 1081 | . 2 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ ((𝜓 ∧ 𝜃) ∧ 𝜂)) | |
7 | df-3an 1081 | . 2 ⊢ ((𝜒 ∧ 𝜏 ∧ 𝜁) ↔ ((𝜒 ∧ 𝜏) ∧ 𝜁)) | |
8 | 5, 6, 7 | 3imtr4g 297 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) → (𝜒 ∧ 𝜏 ∧ 𝜁))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1079 |
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 208 df-an 397 df-3an 1081 |
This theorem is referenced by: pofun 5484 isopolem 7087 issmo2 7975 smores 7978 inawina 10100 gchina 10109 repswcshw 14162 coprmprod 15993 issubmnd 17926 issubg2 18232 issubrg2 19484 issubassa3 20025 ocv2ss 20745 sslm 21835 cmetcaulem 23818 axcontlem4 26680 axcontlem8 26684 redwlk 27381 clwwlknwwlksn 27743 numclwwlk1lem2foa 28060 dipsubdir 28552 subgrpth 32278 cgr3tr4 33410 idinside 33442 ftc1anclem7 34854 fzmul 34897 fdc1 34902 rngosubdi 35104 rngosubdir 35105 cdlemg33a 37722 upwlkwlk 43891 lidlmsgrp 44125 lidlrng 44126 |
Copyright terms: Public domain | W3C validator |