Theorem animorrl 979

Description: Conjunction implies disjunction with one common formula (4/4). (Contributed by BJ, 4-Oct-2019.)

Assertion

Ref	Expression
animorrl	⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∨ 𝜒))

Proof of Theorem animorrl

Step	Hyp	Ref	Expression
1		simpr 484	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
2	1	orcd 872	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∨ 𝜒))

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 846

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 206  df-an 396  df-or 847

This theorem is referenced by:  nelpr1  4657  zzlesq  14201  ccatsymb  14564  sadadd2lem2  16424  mreexexlem4d  17626  drngnidl  21137  ppttop  22909  wilthlem2  27000  bcmono  27209  addsqnreup  27375  mideulem2  28537  linds2eq  33096  fnwe2lem3  42476  fzuntgd  42888  disjxp1  44433  nnfoctbdjlem  45843