![]() |
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 607 | . . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜏))) |
4 | 3anim123d.3 | . . 3 ⊢ (𝜑 → (𝜂 → 𝜁)) | |
5 | 3, 4 | anim12d 607 | . 2 ⊢ (𝜑 → (((𝜓 ∧ 𝜃) ∧ 𝜂) → ((𝜒 ∧ 𝜏) ∧ 𝜁))) |
6 | df-3an 1086 | . 2 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ ((𝜓 ∧ 𝜃) ∧ 𝜂)) | |
7 | df-3an 1086 | . 2 ⊢ ((𝜒 ∧ 𝜏 ∧ 𝜁) ↔ ((𝜒 ∧ 𝜏) ∧ 𝜁)) | |
8 | 5, 6, 7 | 3imtr4g 295 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) → (𝜒 ∧ 𝜏 ∧ 𝜁))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1084 |
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 395 df-3an 1086 |
This theorem is referenced by: pofun 5608 isopolem 7352 issmo2 8370 smores 8373 inawina 10715 gchina 10724 repswcshw 14798 coprmprod 16635 issubmnd 18724 issubg2 19104 issubrng2 20507 issubrg2 20543 rnglidlmsgrp 21153 rnglidlrng 21154 ocv2ss 21622 issubassa3 21816 sslm 23247 cmetcaulem 25260 axcontlem4 28850 axcontlem8 28854 redwlk 29558 clwwlknwwlksn 29920 numclwwlk1lem2foa 30236 dipsubdir 30730 subgrpth 34875 cgr3tr4 35779 idinside 35811 ftc1anclem7 37303 fzmul 37345 fdc1 37350 rngosubdi 37549 rngosubdir 37550 cdlemg33a 40309 upwlkwlk 47387 |
Copyright terms: Public domain | W3C validator |