Theorem 3mix2 1348

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

Syntax hints:   → wi 4   ∨ w3o 1100

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 1102

This theorem is referenced by:  3mix2i  1351  3mix2d  1354  tppreqb  4777  tpres  7200  onzsl  7841  sornom  10260  nnz  12611  nn0le2is012  12659  hash1to3  14528  cshwshashlem1  17154  zabsle1  27425  ostth  27768  nolesgn2o  27800  nogesgn1o  27802  ltssolem1  27804  nosep1o  27810  nosep2o  27811  nodenselem8  27820  fnwe2lem3  43670  dfxlim2v  46452