Theorem animorrl 982

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 873	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∨ 𝜒))

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

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

This theorem is referenced by:  nelpr1  4621  zzlesq  14178  ccatsymb  14554  sadadd2lem2  16427  mreexexlem4d  17615  drngnidl  21160  ppttop  22901  wilthlem2  26986  bcmono  27195  addsqnreup  27361  mideulem2  28668  linds2eq  33359  weiunso  36461  grpods  42189  fnwe2lem3  43048  fzuntgd  43454  disjxp1  45070  nnfoctbdjlem  46460