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  4625  zzlesq  14262  ccatsymb  14640  sadadd2lem2  16533  mreexexlem4d  17728  drngnidl  21414  ppttop  23201  wilthlem2  27270  bcmono  27478  addsqnreup  27644  mideulem2  29052  linds2eq  33725  weiunso  37017  grpods  43001  fnwe2lem3  43819  fzuntgd  44224  disjxp1  45829  nnfoctbdjlem  47209  chnerlem2  47639