Theorem 3mix2 1350

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 1349	. 2 ⊢ (𝜑 → (𝜑 ∨ 𝜒 ∨ 𝜓))
2		3orrot 1108	. 2 ⊢ ((𝜓 ∨ 𝜑 ∨ 𝜒) ↔ (𝜑 ∨ 𝜒 ∨ 𝜓))
3	1, 2	sylibr 237	1 ⊢ (𝜑 → (𝜓 ∨ 𝜑 ∨ 𝜒))

This proof depends on syntax axioms:   → wi 4   ∨ w3o 1102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862  df-3or 1104

This theorem is used by:  3mix2i  1353  3mix2d  1356  tppreqb  4768  tpres  7200  onzsl  7842  sornom  10279  nnz  12636  nn0le2is012  12685  hash1to3  14557  cshwshashlem1  17187  zabsle1  27532  ostth  27875  nolesgn2o  27907  nogesgn1o  27909  ltssolem1  27911  nosep1o  27917  nosep2o  27918  nodenselem8  27927  fnwe2lem3  43893  dfxlim2v  46675