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  4618  zzlesq  14171  ccatsymb  14547  sadadd2lem2  16420  mreexexlem4d  17608  drngnidl  21153  ppttop  22894  wilthlem2  26979  bcmono  27188  addsqnreup  27354  mideulem2  28661  linds2eq  33352  weiunso  36454  grpods  42182  fnwe2lem3  43041  fzuntgd  43447  disjxp1  45063  nnfoctbdjlem  46453