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  4607  zzlesq  14110  ccatsymb  14487  sadadd2lem2  16358  mreexexlem4d  17550  drngnidl  21178  ppttop  22920  wilthlem2  27004  bcmono  27213  addsqnreup  27379  mideulem2  28710  linds2eq  33341  weiunso  36499  grpods  42226  fnwe2lem3  43084  fzuntgd  43490  disjxp1  45105  nnfoctbdjlem  46492