Theorem animorrl 996

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862

This theorem is used by:  nelpr1  4618  zzlesq  14274  ccatsymb  14652  sadadd2lem2  16546  mreexexlem4d  17741  drngnidl  21446  ppttop  23238  wilthlem2  27313  bcmono  27521  addsqnreup  27687  mideulem2  29097  tgaaddcpbl2  29240  linds2eq  33822  weiunso  37093  grpods  43068  fnwe2lem3  43901  fzuntgd  44306  disjxp1  45911  nnfoctbdjlem  47291  chnerlem2  47719