Theorem animorrl 981

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

This theorem is referenced by:  nelpr1  4676  zzlesq  14255  ccatsymb  14630  sadadd2lem2  16496  mreexexlem4d  17705  drngnidl  21276  ppttop  23035  wilthlem2  27130  bcmono  27339  addsqnreup  27505  mideulem2  28760  linds2eq  33374  weiunso  36432  grpods  42151  fnwe2lem3  43009  fzuntgd  43420  disjxp1  44971  nnfoctbdjlem  46376