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

Syntax hints:   → wi 4   ∨ w3o 1085

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 848  df-3or 1087

This theorem is referenced by:  3mix2i  1335  3mix2d  1338  3jaobOLD  1429  tppreqb  4761  tpres  7147  onzsl  7788  sornom  10187  nnz  12509  nn0le2is012  12556  hash1to3  14415  cshwshashlem1  17023  zabsle1  27263  ostth  27606  nolesgn2o  27639  nogesgn1o  27641  ltssolem1  27643  nosep1o  27649  nosep2o  27650  nodenselem8  27659  fnwe2lem3  43294  dfxlim2v  46091