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  4611  fnwe2lem4  8150  zzlesq  14353  ccatsymb  14731  sadadd2lem2  16625  mreexexlem4d  17826  drngnidl  21536  ppttop  23330  wilthlem2  27401  bcmono  27609  addsqnreup  27775  mideulem2  29215  tgaaddcpbl2  29358  linds2eq  33982  weiunso  37346  grpods  43337  fzuntgd  44552  disjxp1  46179  nnfoctbdjlem  47558  chnerlem2  47986