Theorem 3mix2 1330

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

Syntax hints:   → wi 4   ∨ w3o 1085

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 206  df-or 845  df-3or 1087

This theorem is referenced by:  3mix2i  1333  3mix2d  1336  3jaob  1425  tppreqb  4738  tpres  7076  onzsl  7693  sornom  10033  nnssz  12340  nn0le2is012  12384  hash1to3  14205  cshwshashlem1  16797  zabsle1  26444  ostth  26787  nolesgn2o  33874  nogesgn1o  33876  sltsolem1  33878  nosep1o  33884  nosep2o  33885  nodenselem8  33894  fnwe2lem3  40877  dfxlim2v  43388