Theorem 3mix2 1329

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

Syntax hints:   → wi 4   ∨ w3o 1084

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 844  df-3or 1086

This theorem is referenced by:  3mix2i  1332  3mix2d  1335  3jaob  1424  tppreqb  4735  tpres  7058  onzsl  7668  sornom  9964  nnssz  12270  nn0le2is012  12314  hash1to3  14133  cshwshashlem1  16725  zabsle1  26349  ostth  26692  nolesgn2o  33801  nogesgn1o  33803  sltsolem1  33805  nosep1o  33811  nosep2o  33812  nodenselem8  33821  fnwe2lem3  40793  dfxlim2v  43278