Theorem 3mix3 1232

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 1230	. 2 ⊢ (𝜑 → (𝜑 ∨ 𝜓 ∨ 𝜒))
2		3orrot 1044	. 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒 ∨ 𝜑))
3	1, 2	sylib 208	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:  3mix3i  1235  3mix3d  1238  3jaob  1390  tpid3gOLD  4306  tppreqb  4336  tpres  6466  onzsl  7046  sornom  9099  fpwwe2lem13  9464  nn0le2is012  11441  nn01to3  11781  qbtwnxr  12031  hash1to3  13273  cshwshashlem1  15802  ostth  25328  nolesgn2o  31824  sltsolem1  31826  btwncolinear1  32176  tpid3gVD  39077  limcicciooub  39869  dfxlim2v  40073  pfxnd  41395