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  4659  zzlesq  14242  ccatsymb  14617  sadadd2lem2  16484  mreexexlem4d  17692  drngnidl  21271  ppttop  23030  wilthlem2  27127  bcmono  27336  addsqnreup  27502  mideulem2  28757  linds2eq  33389  weiunso  36449  grpods  42176  fnwe2lem3  43041  fzuntgd  43448  disjxp1  45009  nnfoctbdjlem  46411