Theorem animorrl 996

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 490	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
2	1	orcd 887	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∨ 𝜒))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862

This theorem is used by:  nelpr1  4615  fnwe2lem4  8175  zzlesq  14377  ccatsymb  14755  sadadd2lem2  16649  mreexexlem4d  17850  drngnidl  21561  ppttop  23355  wilthlem2  27426  bcmono  27634  addsqnreup  27800  mideulem2  29240  tgaaddcpbl2  29383  linds2eq  34006  weiunso  37432  grpods  43436  fzuntgd  44651  disjxp1  46291  nnfoctbdjlem  47670  chnerlem2  48098