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  zzlesq  14330  ccatsymb  14708  sadadd2lem2  16600  mreexexlem4d  17801  drngnidl  21511  ppttop  23305  wilthlem2  27378  bcmono  27586  addsqnreup  27752  mideulem2  29192  tgaaddcpbl2  29335  linds2eq  33918  weiunso  37224  grpods  43212  fnwe2lem3  44012  fzuntgd  44417  disjxp1  46029  nnfoctbdjlem  47409  chnerlem2  47837