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 858 | . 2 ⊢ (𝜑 → (¬ 𝜓 → 𝜒)) |
3 | 2 | imp 407 | 1 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 ∨ wo 841 |
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 208 df-an 397 df-or 842 |
This theorem is referenced by: elunnel1 4123 bren2 8528 php 8689 unxpdomlem3 8712 tcrank 9301 dfac12lem1 9557 dfac12lem2 9558 ttukeylem3 9921 ttukeylem5 9923 ttukeylem6 9924 xrmax2 12557 xrmin1 12558 xrge0nre 12829 ccatco 14185 pcgcd 16202 mreexexd 16907 tsrlemax 17818 gsumval2 17884 xrsdsreval 20518 xrsdsreclb 20520 xrsxmet 23344 elii2 23467 xrhmeo 23477 pcoass 23555 limccnp 24416 logreclem 25267 eldmgm 25526 lgsdir2 25833 colmid 26401 outpasch 26468 lmiisolem 26509 elpreq 30217 fzne1 30437 esumcvgre 31249 ballotlem2 31645 lclkrlem2h 38530 aomclem5 39536 cvgdvgrat 40522 bccbc 40554 elunnel2 41173 stoweidlem26 42188 stoweidlem34 42196 fourierswlem 42392 |
Copyright terms: Public domain | W3C validator |