Theorem animorrl 983

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 848

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 207  df-an 396  df-or 849

This theorem is referenced by:  nelpr1  4613  zzlesq  14141  ccatsymb  14518  sadadd2lem2  16389  mreexexlem4d  17582  drngnidl  21210  ppttop  22963  wilthlem2  27047  bcmono  27256  addsqnreup  27422  mideulem2  28818  linds2eq  33473  weiunso  36679  grpods  42558  fnwe2lem3  43403  fzuntgd  43808  disjxp1  45423  nnfoctbdjlem  46807  chnerlem2  47235