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  4635  zzlesq  14229  ccatsymb  14605  sadadd2lem2  16474  mreexexlem4d  17664  drngnidl  21209  ppttop  22950  wilthlem2  27036  bcmono  27245  addsqnreup  27411  mideulem2  28718  linds2eq  33401  weiunso  36489  grpods  42212  fnwe2lem3  43043  fzuntgd  43449  disjxp1  45060  nnfoctbdjlem  46451