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  4608  zzlesq  14131  ccatsymb  14507  sadadd2lem2  16379  mreexexlem4d  17571  drngnidl  21168  ppttop  22910  wilthlem2  26995  bcmono  27204  addsqnreup  27370  mideulem2  28697  linds2eq  33328  weiunso  36439  grpods  42167  fnwe2lem3  43025  fzuntgd  43431  disjxp1  45047  nnfoctbdjlem  46437