Theorem animorrl 996

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 489	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
2	1	orcd 886	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∨ 𝜒))

Syntax hints:   → wi 4   ∧ wa 400   ∨ wo 860

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 210  df-an 401  df-or 861

This theorem is referenced by:  nelpr1  4616  zzlesq  14233  ccatsymb  14610  sadadd2lem2  16498  mreexexlem4d  17693  drngnidl  21342  ppttop  23125  wilthlem2  27191  bcmono  27399  addsqnreup  27565  mideulem2  28965  linds2eq  33610  weiunso  36839  grpods  42823  fnwe2lem3  43641  fzuntgd  44046  disjxp1  45647  nnfoctbdjlem  47027  chnerlem2  47457