Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3mix3 | Structured version Visualization version GIF version |
Description: Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.) |
Ref | Expression |
---|---|
3mix3 | ⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3mix1 1223 | . 2 ⊢ (𝜑 → (𝜑 ∨ 𝜓 ∨ 𝜒)) | |
2 | 3orrot 1037 | . 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒 ∨ 𝜑)) | |
3 | 1, 2 | sylib 207 | 1 ⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ w3o 1030 |
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-or 384 df-3or 1032 |
This theorem is referenced by: 3mix3i 1228 3mix3d 1231 3jaob 1382 tpid3gOLD 4249 tppreqb 4277 tpres 6371 onzsl 6938 sornom 8982 fpwwe2lem13 9343 nn01to3 11657 qbtwnxr 11905 hash1to3 13128 cshwshashlem1 15640 ostth 25128 sltsolem1 31067 btwncolinear1 31346 tpid3gVD 38099 limcicciooub 38704 pfxnd 40258 nn0le2is012 41938 |
Copyright terms: Public domain | W3C validator |