Theorem orcanai 990

Description: Change disjunction in consequent to conjunction in antecedent. (Contributed by NM, 8-Jun-1994.)

Hypothesis

Ref	Expression
orcanai.1	⊢ (𝜑 → (𝜓 ∨ 𝜒))

Assertion

Ref	Expression
orcanai	⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒)

Proof of Theorem orcanai

Step	Hyp	Ref	Expression
1		orcanai.1	. . 3 ⊢ (𝜑 → (𝜓 ∨ 𝜒))
2	1	ord 391	. 2 ⊢ (𝜑 → (¬ 𝜓 → 𝜒))
3	2	imp 444	1 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒)

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 382   ∧ wa 383

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 197  df-or 384  df-an 385

This theorem is referenced by:  elunnel1  3898  bren2  8155  php  8312  unxpdomlem3  8334  tcrank  8923  dfac12lem1  9178  dfac12lem2  9179  ttukeylem3  9546  ttukeylem5  9548  ttukeylem6  9549  xrmax2  12221  xrmin1  12222  xrge0nre  12491  ccatco  13802  pcgcd  15805  mreexexd  16531  tsrlemax  17442  gsumval2  17502  xrsdsreval  20014  xrsdsreclb  20016  xrsxmet  22834  elii2  22957  xrhmeo  22967  pcoass  23045  limccnp  23875  logreclem  24721  eldmgm  24969  lgsdir2  25276  colmid  25804  lmiisolem  25909  elpreq  29689  esumcvgre  30484  eulerpartlemgvv  30769  ballotlem2  30881  lclkrlem2h  37324  aomclem5  38149  cvgdvgrat  39033  bccbc  39065  elunnel2  39716  stoweidlem26  40765  stoweidlem34  40773  fourierswlem  40969