Theorem 3mix2 1332

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

Syntax hints:   → wi 4   ∨ w3o 1087

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 210  df-or 847  df-3or 1089

This theorem is referenced by:  3mix2i  1335  3mix2d  1338  3jaob  1427  tppreqb  4703  tpres  6985  onzsl  7592  sornom  9789  nnssz  12095  nn0le2is012  12139  hash1to3  13955  cshwshashlem1  16544  zabsle1  26044  ostth  26387  nolesgn2o  33529  nogesgn1o  33531  sltsolem1  33533  nosep1o  33539  nosep2o  33540  nodenselem8  33549  fnwe2lem3  40489  dfxlim2v  42970