Theorem 3mix2 1333

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

Syntax hints:   → wi 4   ∨ w3o 1086

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 207  df-or 849  df-3or 1088

This theorem is referenced by:  3mix2i  1336  3mix2d  1339  3jaobOLD  1430  tppreqb  4749  tpres  7150  onzsl  7791  sornom  10193  nnz  12539  nn0le2is012  12587  hash1to3  14448  cshwshashlem1  17060  zabsle1  27276  ostth  27619  nolesgn2o  27652  nogesgn1o  27654  ltssolem1  27656  nosep1o  27662  nosep2o  27663  nodenselem8  27672  fnwe2lem3  43501  dfxlim2v  46296