Theorem 3mix2 1231

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

Syntax hints:   → wi 4   ∨ w3o 1036

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 385  df-3or 1038

This theorem is referenced by:  3mix2i  1234  3mix2d  1237  3jaob  1390  tppreqb  4336  tpres  6466  onzsl  7046  sornom  9099  nn0le2is012  11441  hash1to3  13273  cshwshashlem1  15802  zabsle1  25021  ostth  25328  nolesgn2o  31824  sltsolem1  31826  nosep1o  31832  nodenselem8  31841  fnwe2lem3  37622  dfxlim2v  40073