Theorem animorrl 993

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

Syntax hints:   → wi 4   ∧ wa 399   ∨ wo 858

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 209  df-an 400  df-or 859

This theorem is referenced by:  nelpr1  4612  zzlesq  14216  ccatsymb  14593  sadadd2lem2  16467  mreexexlem4d  17662  drngnidl  21293  ppttop  23047  wilthlem2  27110  bcmono  27318  addsqnreup  27484  mideulem2  28880  linds2eq  33528  weiunso  36790  grpods  42775  fnwe2lem3  43593  fzuntgd  43998  disjxp1  45613  nnfoctbdjlem  46993  chnerlem2  47423