Theorem 3mix1 1223

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

Assertion

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

Proof of Theorem 3mix1

Step	Hyp	Ref	Expression
1		orc 399	. 2 ⊢ (𝜑 → (𝜑 ∨ (𝜓 ∨ 𝜒)))
2		3orass 1034	. 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))
3	1, 2	sylibr 223	1 ⊢ (𝜑 → (𝜑 ∨ 𝜓 ∨ 𝜒))

Syntax hints:   → wi 4   ∨ wo 382   ∨ 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:  3mix2  1224  3mix3  1225  3mix1i  1226  3mix1d  1229  3jaob  1382  tppreqb  4277  onzsl  6938  sornom  8982  fpwwe2lem13  9343  hashv01gt1  12995  hash1to3  13128  cshwshashlem1  15640  zabsle1  24821  colinearalg  25590  frgraregorufr0  26579  sltsolem1  31067  frege129d  37074  frgrregorufr0  41489  nn0le2is012  41938