|   | 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 865 | . 2 ⊢ (𝜑 → (¬ 𝜓 → 𝜒)) | 
| 3 | 2 | imp 406 | 1 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∨ wo 848 | 
| 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 207 df-an 396 df-or 849 | 
| This theorem is referenced by: elunnel1 4154 elunnel2 4155 bren2 9023 php 9247 phpOLD 9259 unxpdomlem3 9288 tcrank 9924 dfac12lem1 10184 dfac12lem2 10185 ttukeylem3 10551 ttukeylem5 10553 ttukeylem6 10554 xrmax2 13218 xrmin1 13219 xrge0nre 13493 fzne1 13644 ccatco 14874 pcgcd 16916 mreexexd 17691 tsrlemax 18631 gsumval2 18699 xrsdsreval 21429 xrsdsreclb 21431 xrsxmet 24831 elii2 24965 xrhmeo 24977 pcoass 25057 limccnp 25926 logreclem 26805 eldmgm 27065 lgsdir2 27374 maxs2 27811 mins1 27812 colmid 28696 outpasch 28763 lmiisolem 28804 elpreq 32548 2exple2exp 32834 irredminply 33757 esumcvgre 34092 ballotlem2 34491 lclkrlem2h 41516 aomclem5 43070 cvgdvgrat 44332 bccbc 44364 stoweidlem26 46041 stoweidlem34 46049 fourierswlem 46245 | 
| Copyright terms: Public domain | W3C validator |