Theorem 3mix2 1338

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

Syntax hints:   → wi 4   ∨ w3o 1091

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 208  df-or 854  df-3or 1093

This theorem is referenced by:  3mix2i  1341  3mix2d  1344  3jaobOLD  1435  tppreqb  4738  tpres  7145  onzsl  7786  sornom  10190  nnz  12536  nn0le2is012  12584  hash1to3  14445  cshwshashlem1  17057  zabsle1  27277  ostth  27620  nolesgn2o  27653  nogesgn1o  27655  ltssolem1  27657  nosep1o  27663  nosep2o  27664  nodenselem8  27673  fnwe2lem3  43497  dfxlim2v  46290