Theorem 3mix3 1225

Description: Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)

Assertion

Ref	Expression
3mix3	⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜑))

Proof of Theorem 3mix3

Step	Hyp	Ref	Expression
1		3mix1 1223	. 2 ⊢ (𝜑 → (𝜑 ∨ 𝜓 ∨ 𝜒))
2		3orrot 1037	. 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒 ∨ 𝜑))
3	1, 2	sylib 207	1 ⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜑))

Syntax hints:   → wi 4   ∨ w3o 1030

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 196  df-or 384  df-3or 1032

This theorem is referenced by:  3mix3i  1228  3mix3d  1231  3jaob  1382  tpid3gOLD  4249  tppreqb  4277  tpres  6371  onzsl  6938  sornom  8982  fpwwe2lem13  9343  nn01to3  11657  qbtwnxr  11905  hash1to3  13128  cshwshashlem1  15640  ostth  25128  sltsolem1  31067  btwncolinear1  31346  tpid3gVD  38099  limcicciooub  38704  pfxnd  40258  nn0le2is012  41938