Theorem 3mix2 1327

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

Syntax hints:   → wi 4   ∨ w3o 1082

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 209  df-or 844  df-3or 1084

This theorem is referenced by:  3mix2i  1330  3mix2d  1333  3jaob  1422  tppreqb  4740  tpres  6965  onzsl  7563  sornom  9701  nnssz  12005  nn0le2is012  12049  hash1to3  13852  cshwshashlem1  16431  zabsle1  25874  ostth  26217  nolesgn2o  33180  sltsolem1  33182  nosep1o  33188  nodenselem8  33197  fnwe2lem3  39659  dfxlim2v  42135