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 485	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
2	1	orcd 871	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∨ 𝜒))

Syntax hints:   → wi 4   ∧ wa 396   ∨ wo 845

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 397  df-or 846

This theorem is referenced by:  nelpr1  4656  zzlesq  14169  ccatsymb  14531  sadadd2lem2  16390  mreexexlem4d  17590  drngnidl  20853  ppttop  22509  wilthlem2  26570  bcmono  26777  addsqnreup  26943  mideulem2  27982  linds2eq  32492  fnwe2lem3  41784  fzuntgd  42199  disjxp1  43746  nnfoctbdjlem  45161