Theorem 3mix3 1331

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 1329	. 2 ⊢ (𝜑 → (𝜑 ∨ 𝜓 ∨ 𝜒))
2		3orrot 1091	. 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒 ∨ 𝜑))
3	1, 2	sylib 218	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:  3mix3i  1334  3mix3d  1337  3jaobOLD  1426  tppreqb  4809  tpres  7220  onzsl  7866  sornom  10314  fpwwe2lem12  10679  nn0le2is012  12679  nn01to3  12980  qbtwnxr  13238  hash1to3  14527  swrdnd0  14691  pfxnd  14721  cshwshashlem1  17129  ostth  27697  nolesgn2o  27730  sltsolem1  27734  nosep2o  27741  btwncolinear1  36050  tpid3gVD  44839  limcicciooub  45592  dfxlim2v  45802