Theorem animorrl 982

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

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

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 848

This theorem is referenced by:  nelpr1  4611  zzlesq  14129  ccatsymb  14506  sadadd2lem2  16377  mreexexlem4d  17570  drngnidl  21198  ppttop  22951  wilthlem2  27035  bcmono  27244  addsqnreup  27410  mideulem2  28806  linds2eq  33462  weiunso  36660  grpods  42444  fnwe2lem3  43290  fzuntgd  43695  disjxp1  45310  nnfoctbdjlem  46695  chnerlem2  47123