Theorem 3mix2 1333

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

Syntax hints:   → wi 4   ∨ w3o 1086

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 207  df-or 849  df-3or 1088

This theorem is referenced by:  3mix2i  1336  3mix2d  1339  3jaobOLD  1430  tppreqb  4763  tpres  7157  onzsl  7798  sornom  10199  nnz  12521  nn0le2is012  12568  hash1to3  14427  cshwshashlem1  17035  zabsle1  27275  ostth  27618  nolesgn2o  27651  nogesgn1o  27653  ltssolem1  27655  nosep1o  27661  nosep2o  27662  nodenselem8  27671  fnwe2lem3  43409  dfxlim2v  46205