Theorem 3mix3d 1339

Description: Deduction introducing triple disjunction. (Contributed by Scott Fenton, 8-Jun-2011.)

Hypothesis

Ref	Expression
3mixd.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
3mix3d	⊢ (𝜑 → (𝜒 ∨ 𝜃 ∨ 𝜓))

Proof of Theorem 3mix3d

Step	Hyp	Ref	Expression
1		3mixd.1	. 2 ⊢ (𝜑 → 𝜓)
2		3mix3 1333	. 2 ⊢ (𝜓 → (𝜒 ∨ 𝜃 ∨ 𝜓))
3	1, 2	syl 17	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:  xpord3inddlem  8084  elfiun  9314  nnnegz  12471  fvf1tp  13693  hashv01gt1  14252  lcmfunsnlem2lem2  16550  cshwshashlem1  17007  dyaddisjlem  25523  zabsle1  27234  noextendgt  27609  sltsolem1  27614  nodense  27631  btwncolg3  28535  btwnlng3  28599  frgr3vlem2  30254  3vfriswmgr  30258  frgrregorufr0  30304  constrcccllem  33767  weiunso  36510  fnwe2lem3  43144  omcl2  43425  gpgprismgriedgdmss  48151  gpgedgvtx1  48161  gpgvtxedg0  48162  gpgvtxedg1  48163  gpg3kgrtriexlem6  48187  gpgprismgr4cycllem3  48196  eenglngeehlnmlem2  48838