Theorem 3mix2 1368

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

Syntax hints:   → wi 4   ∨ w3o 1071

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 197  df-or 384  df-3or 1073

This theorem is referenced by:  3mix2i  1371  3mix2d  1374  3jaob  1503  tppreqb  4444  tpres  6582  onzsl  7163  sornom  9212  nn0le2is012  11554  hash1to3  13386  cshwshashlem1  15925  zabsle1  25141  ostth  25448  nolesgn2o  32051  sltsolem1  32053  nosep1o  32059  nodenselem8  32068  fnwe2lem3  38041  dfxlim2v  40493