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  4599  zzlesq  14159  ccatsymb  14536  sadadd2lem2  16410  mreexexlem4d  17604  drngnidl  21233  ppttop  22982  wilthlem2  27046  bcmono  27254  addsqnreup  27420  mideulem2  28816  linds2eq  33456  weiunso  36664  grpods  42647  fnwe2lem3  43498  fzuntgd  43903  disjxp1  45518  nnfoctbdjlem  46901  chnerlem2  47329