Theorem 3mix2 1345

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

Syntax hints:   → wi 4   ∨ w3o 1097

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 209  df-or 859  df-3or 1099

This theorem is referenced by:  3mix2i  1348  3mix2d  1351  3jaobOLD  1446  tppreqb  4765  tpres  7185  onzsl  7826  sornom  10234  nnz  12589  nn0le2is012  12637  hash1to3  14505  cshwshashlem1  17131  zabsle1  27357  ostth  27700  nolesgn2o  27732  nogesgn1o  27734  ltssolem1  27736  nosep1o  27742  nosep2o  27743  nodenselem8  27752  fnwe2lem3  43626  dfxlim2v  46418