Theorem animorrl 979

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

Syntax hints:   → wi 4   ∧ wa 396   ∨ wo 845

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 206  df-an 397  df-or 846

This theorem is referenced by:  nelpr1  4656  zzlesq  14172  ccatsymb  14534  sadadd2lem2  16393  mreexexlem4d  17593  drngnidl  20860  ppttop  22517  wilthlem2  26580  bcmono  26787  addsqnreup  26953  mideulem2  28023  linds2eq  32542  fnwe2lem3  41876  fzuntgd  42291  disjxp1  43838  nnfoctbdjlem  45250