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  4630  zzlesq  14222  ccatsymb  14598  sadadd2lem2  16467  mreexexlem4d  17657  drngnidl  21202  ppttop  22943  wilthlem2  27029  bcmono  27238  addsqnreup  27404  mideulem2  28659  linds2eq  33342  weiunso  36430  grpods  42153  fnwe2lem3  43023  fzuntgd  43429  disjxp1  45041  nnfoctbdjlem  46432