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  4606  zzlesq  14115  ccatsymb  14492  sadadd2lem2  16363  mreexexlem4d  17555  drngnidl  21182  ppttop  22923  wilthlem2  27007  bcmono  27216  addsqnreup  27382  mideulem2  28713  linds2eq  33353  weiunso  36531  grpods  42307  fnwe2lem3  43169  fzuntgd  43575  disjxp1  45190  nnfoctbdjlem  46577  chnerlem2  47005