Theorem 3mix2 1331

Description: Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)

Assertion

Ref	Expression
3mix2	⊢ (𝜑 → (𝜓 ∨ 𝜑 ∨ 𝜒))

Proof of Theorem 3mix2

Step	Hyp	Ref	Expression
1		3mix1 1330	. 2 ⊢ (𝜑 → (𝜑 ∨ 𝜒 ∨ 𝜓))
2		3orrot 1092	. 2 ⊢ ((𝜓 ∨ 𝜑 ∨ 𝜒) ↔ (𝜑 ∨ 𝜒 ∨ 𝜓))
3	1, 2	sylibr 234	1 ⊢ (𝜑 → (𝜓 ∨ 𝜑 ∨ 𝜒))

Syntax hints:   → wi 4   ∨ 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-or 847  df-3or 1088

This theorem is referenced by:  3mix2i  1334  3mix2d  1337  3jaobOLD  1427  tppreqb  4830  tpres  7238  onzsl  7883  sornom  10346  nnz  12660  nn0le2is012  12707  hash1to3  14541  cshwshashlem1  17143  zabsle1  27358  ostth  27701  nolesgn2o  27734  nogesgn1o  27736  sltsolem1  27738  nosep1o  27744  nosep2o  27745  nodenselem8  27754  fnwe2lem3  43009  dfxlim2v  45768