Theorem orcanai 1005

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 865	. 2 ⊢ (𝜑 → (¬ 𝜓 → 𝜒))
3	2	imp 406	1 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒)

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