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  4807  tpres  7203  onzsl  7837  sornom  10274  nnz  12583  nn0le2is012  12630  hash1to3  14456  cshwshashlem1  17033  zabsle1  27035  ostth  27378  nolesgn2o  27410  nogesgn1o  27412  sltsolem1  27414  nosep1o  27420  nosep2o  27421  nodenselem8  27430  fnwe2lem3  42096  dfxlim2v  44861