| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > 3orim123d | Structured version Visualization version GIF version | ||
| Description: Deduction joining 3 implications to form implication of disjunctions. (Contributed by NM, 4-Apr-1997.) |
| Ref | Expression |
|---|---|
| 3anim123d.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
| 3anim123d.2 | ⊢ (𝜑 → (𝜃 → 𝜏)) |
| 3anim123d.3 | ⊢ (𝜑 → (𝜂 → 𝜁)) |
| Ref | Expression |
|---|---|
| 3orim123d | ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜂) → (𝜒 ∨ 𝜏 ∨ 𝜁))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 3anim123d.1 | . . . 4 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
| 2 | 3anim123d.2 | . . . 4 ⊢ (𝜑 → (𝜃 → 𝜏)) | |
| 3 | 1, 2 | orim12d 967 | . . 3 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏))) |
| 4 | 3anim123d.3 | . . 3 ⊢ (𝜑 → (𝜂 → 𝜁)) | |
| 5 | 3, 4 | orim12d 967 | . 2 ⊢ (𝜑 → (((𝜓 ∨ 𝜃) ∨ 𝜂) → ((𝜒 ∨ 𝜏) ∨ 𝜁))) |
| 6 | df-3or 1088 | . 2 ⊢ ((𝜓 ∨ 𝜃 ∨ 𝜂) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂)) | |
| 7 | df-3or 1088 | . 2 ⊢ ((𝜒 ∨ 𝜏 ∨ 𝜁) ↔ ((𝜒 ∨ 𝜏) ∨ 𝜁)) | |
| 8 | 5, 6, 7 | 3imtr4g 296 | 1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜂) → (𝜒 ∨ 𝜏 ∨ 𝜁))) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∨ wo 848 ∨ w3o 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-or 849 df-3or 1088 |
| This theorem is referenced by: fr3nr 7792 soxp 8154 poxp3 8175 zorn2lem6 10541 fpwwe2lem11 10681 fpwwe2lem12 10682 sltres 27707 colinearalglem4 28924 chnso 33004 constrconj 33786 colinearxfr 36076 weiunso 36467 fin2so 37614 frege133d 43778 el1fzopredsuc 47337 fmtno4prmfac 47559 |
| Copyright terms: Public domain | W3C validator |