![]() |
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 1088 | . 2 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ ((𝜓 ∧ 𝜃) ∧ 𝜂)) | |
7 | df-3an 1088 | . 2 ⊢ ((𝜒 ∧ 𝜏 ∧ 𝜁) ↔ ((𝜒 ∧ 𝜏) ∧ 𝜁)) | |
8 | 5, 6, 7 | 3imtr4g 296 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) → (𝜒 ∧ 𝜏 ∧ 𝜁))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 |
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 1088 |
This theorem is referenced by: pofun 5614 isopolem 7364 issmo2 8387 smores 8390 inawina 10727 gchina 10736 repswcshw 14846 coprmprod 16694 issubmnd 18786 issubg2 19171 issubrng2 20574 issubrg2 20608 rnglidlmsgrp 21273 rnglidlrng 21274 ocv2ss 21708 issubassa3 21903 sslm 23322 cmetcaulem 25335 axcontlem4 28996 axcontlem8 29000 redwlk 29704 clwwlknwwlksn 30066 numclwwlk1lem2foa 30382 dipsubdir 30876 constrconj 33749 subgrpth 35118 cgr3tr4 36033 idinside 36065 ftc1anclem7 37685 fzmul 37727 fdc1 37732 rngosubdi 37931 rngosubdir 37932 cdlemg33a 40688 grtrimap 47850 grimgrtri 47851 grlimgrtri 47898 upwlkwlk 47982 |
Copyright terms: Public domain | W3C validator |