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 ⊢ (𝜑 → (𝜓 ∨ 𝜑 ∨ 𝜒))

Syntax hints:   → wi 4   ∨ w3o 1102

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 210  df-or 861  df-3or 1104

This theorem is referenced by:  3mix2i  1353  3mix2d  1356  tppreqb  4773  tpres  7199  onzsl  7838  sornom  10256  nnz  12607  nn0le2is012  12655  hash1to3  14525  cshwshashlem1  17150  zabsle1  27460  ostth  27803  nolesgn2o  27835  nogesgn1o  27837  ltssolem1  27839  nosep1o  27845  nosep2o  27846  nodenselem8  27855  fnwe2lem3  43779  dfxlim2v  46561