Theorem animorrl 988

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 879	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∨ 𝜒))

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

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 208  df-an 397  df-or 854

This theorem is referenced by:  nelpr1  4593  zzlesq  14166  ccatsymb  14543  sadadd2lem2  16417  mreexexlem4d  17611  drngnidl  21243  ppttop  22997  wilthlem2  27057  bcmono  27265  addsqnreup  27431  mideulem2  28827  linds2eq  33471  weiunso  36701  grpods  42686  fnwe2lem3  43504  fzuntgd  43909  disjxp1  45524  nnfoctbdjlem  46905  chnerlem2  47335