![]() |
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 861 | . 2 ⊢ (𝜑 → (¬ 𝜓 → 𝜒)) |
3 | 2 | imp 406 | 1 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∨ wo 844 |
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 396 df-or 845 |
This theorem is referenced by: elunnel1 4141 elunnel2 4142 bren2 8974 php 9205 phpOLD 9217 unxpdomlem3 9247 tcrank 9874 dfac12lem1 10133 dfac12lem2 10134 ttukeylem3 10501 ttukeylem5 10503 ttukeylem6 10504 xrmax2 13151 xrmin1 13152 xrge0nre 13426 ccatco 14782 pcgcd 16807 mreexexd 17588 tsrlemax 18538 gsumval2 18606 xrsdsreval 21269 xrsdsreclb 21271 xrsxmet 24635 elii2 24769 xrhmeo 24781 pcoass 24861 limccnp 25730 logreclem 26598 eldmgm 26858 lgsdir2 27167 maxs2 27603 mins1 27604 colmid 28363 outpasch 28430 lmiisolem 28471 elpreq 32191 fzne1 32423 esumcvgre 33544 ballotlem2 33942 lclkrlem2h 40841 aomclem5 42255 cvgdvgrat 43527 bccbc 43559 stoweidlem26 45193 stoweidlem34 45201 fourierswlem 45397 |
Copyright terms: Public domain | W3C validator |