Theorem animorrl 983

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

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

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 849

This theorem is referenced by:  nelpr1  4598  zzlesq  14168  ccatsymb  14545  sadadd2lem2  16419  mreexexlem4d  17613  drngnidl  21241  ppttop  22972  wilthlem2  27032  bcmono  27240  addsqnreup  27406  mideulem2  28802  linds2eq  33441  weiunso  36648  grpods  42633  fnwe2lem3  43480  fzuntgd  43885  disjxp1  45500  nnfoctbdjlem  46883  chnerlem2  47313