![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > animorrl | Structured version Visualization version GIF version |
Description: Conjunction implies disjunction with one common formula (4/4). (Contributed by BJ, 4-Oct-2019.) |
Ref | Expression |
---|---|
animorrl | ⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∨ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr 486 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓) | |
2 | 1 | orcd 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 |