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  4808  tpres  7204  onzsl  7839  sornom  10278  nnz  12586  nn0le2is012  12633  hash1to3  14459  cshwshashlem1  17036  zabsle1  27142  ostth  27485  nolesgn2o  27517  nogesgn1o  27519  sltsolem1  27521  nosep1o  27527  nosep2o  27528  nodenselem8  27537  fnwe2lem3  42257  dfxlim2v  45022