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 1091	. 2 ⊢ ((𝜓 ∨ 𝜑 ∨ 𝜒) ↔ (𝜑 ∨ 𝜒 ∨ 𝜓))
3	1, 2	sylibr 234	1 ⊢ (𝜑 → (𝜓 ∨ 𝜑 ∨ 𝜒))

Syntax hints:   → wi 4   ∨ w3o 1085

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 848  df-3or 1087

This theorem is referenced by:  3mix2i  1334  3mix2d  1337  3jaobOLD  1428  tppreqb  4787  tpres  7204  onzsl  7850  sornom  10300  nnz  12618  nn0le2is012  12666  hash1to3  14514  cshwshashlem1  17116  zabsle1  27295  ostth  27638  nolesgn2o  27671  nogesgn1o  27673  sltsolem1  27675  nosep1o  27681  nosep2o  27682  nodenselem8  27691  fnwe2lem3  43009  dfxlim2v  45807