![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > orcanai | Structured version Visualization version GIF version |
Description: Change disjunction in consequent to conjunction in antecedent. (Contributed by NM, 8-Jun-1994.) |
Ref | Expression |
---|---|
orcanai.1 | ⊢ (𝜑 → (𝜓 ∨ 𝜒)) |
Ref | Expression |
---|---|
orcanai | ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orcanai.1 | . . 3 ⊢ (𝜑 → (𝜓 ∨ 𝜒)) | |
2 | 1 | ord 897 | . 2 ⊢ (𝜑 → (¬ 𝜓 → 𝜒)) |
3 | 2 | imp 397 | 1 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 386 ∨ wo 880 |
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 199 df-an 387 df-or 881 |
This theorem is referenced by: elunnel1 3980 bren2 8252 php 8412 unxpdomlem3 8434 tcrank 9023 dfac12lem1 9279 dfac12lem2 9280 ttukeylem3 9647 ttukeylem5 9649 ttukeylem6 9650 xrmax2 12294 xrmin1 12295 xrge0nre 12566 ccatco 13955 pcgcd 15952 mreexexd 16660 tsrlemax 17572 gsumval2 17632 xrsdsreval 20150 xrsdsreclb 20152 xrsxmet 22981 elii2 23104 xrhmeo 23114 pcoass 23192 limccnp 24053 logreclem 24901 eldmgm 25160 lgsdir2 25467 colmid 25999 lmiisolem 26104 elpreq 29907 esumcvgre 30697 eulerpartlemgvv 30982 ballotlem2 31095 lclkrlem2h 37588 aomclem5 38470 cvgdvgrat 39351 bccbc 39383 elunnel2 40015 stoweidlem26 41036 stoweidlem34 41044 fourierswlem 41240 |
Copyright terms: Public domain | W3C validator |