MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  animorrl Structured version   Visualization version   GIF version

Theorem animorrl 980
Description: Conjunction implies disjunction with one common formula (4/4). (Contributed by BJ, 4-Oct-2019.)
Assertion
Ref Expression
animorrl ((𝜑𝜓) → (𝜓𝜒))

Proof of Theorem animorrl
StepHypRef Expression
1 simpr 486 . 2 ((𝜑𝜓) → 𝜓)
21orcd 872 1 ((𝜑𝜓) → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wo 846
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 206  df-an 398  df-or 847
This theorem is referenced by:  nelpr1  4619  zzlesq  14117  ccatsymb  14477  sadadd2lem2  16337  mreexexlem4d  17534  drngnidl  20715  ppttop  22373  wilthlem2  26434  bcmono  26641  addsqnreup  26807  mideulem2  27718  linds2eq  32208  fnwe2lem3  41408  fzuntgd  41804  disjxp1  43351  nnfoctbdjlem  44770
  Copyright terms: Public domain W3C validator