![]() |
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 584 | . . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜏))) |
4 | 3anim123d.3 | . . 3 ⊢ (𝜑 → (𝜂 → 𝜁)) | |
5 | 3, 4 | anim12d 584 | . 2 ⊢ (𝜑 → (((𝜓 ∧ 𝜃) ∧ 𝜂) → ((𝜒 ∧ 𝜏) ∧ 𝜁))) |
6 | df-3an 1033 | . 2 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ ((𝜓 ∧ 𝜃) ∧ 𝜂)) | |
7 | df-3an 1033 | . 2 ⊢ ((𝜒 ∧ 𝜏 ∧ 𝜁) ↔ ((𝜒 ∧ 𝜏) ∧ 𝜁)) | |
8 | 5, 6, 7 | 3imtr4g 284 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) → (𝜒 ∧ 𝜏 ∧ 𝜁))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1031 |
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 196 df-an 385 df-3an 1033 |
This theorem is referenced by: pofun 4975 isopolem 6495 issmo2 7333 smores 7336 inawina 9391 gchina 9400 repswcshw 13409 coprmprod 15213 issubmnd 17141 issubg2 17432 issubrg2 18623 ocv2ss 19836 sslm 20913 cmetcaulem 22894 axcontlem4 25647 axcontlem8 25651 redwlk 26136 3cycl3dv 26170 3v3e3cycl1 26172 constr3trllem5 26182 el2wlkonotot0 26399 dipsubdir 27087 cgr3tr4 31329 idinside 31361 ftc1anclem7 32661 fzmul 32707 fdc1 32712 rngosubdi 32914 rngosubdir 32915 cdlemg33a 35012 wlk1wlk 40846 red1wlk 40881 lidlmsgrp 41716 lidlrng 41717 |
Copyright terms: Public domain | W3C validator |