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  4621  zzlesq  14244  ccatsymb  14622  sadadd2lem2  16509  mreexexlem4d  17704  drngnidl  21358  ppttop  23145  wilthlem2  27211  bcmono  27419  addsqnreup  27585  mideulem2  28993  linds2eq  33672  weiunso  36955  grpods  42939  fnwe2lem3  43759  fzuntgd  44164  disjxp1  45769  nnfoctbdjlem  47149  chnerlem2  47579