Theorem orcanai 999

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398   ∨ wo 843

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 209  df-an 399  df-or 844

This theorem is referenced by:  elunnel1  4128  bren2  8542  php  8703  unxpdomlem3  8726  tcrank  9315  dfac12lem1  9571  dfac12lem2  9572  ttukeylem3  9935  ttukeylem5  9937  ttukeylem6  9938  xrmax2  12572  xrmin1  12573  xrge0nre  12844  ccatco  14199  pcgcd  16216  mreexexd  16921  tsrlemax  17832  gsumval2  17898  xrsdsreval  20592  xrsdsreclb  20594  xrsxmet  23419  elii2  23542  xrhmeo  23552  pcoass  23630  limccnp  24491  logreclem  25342  eldmgm  25601  lgsdir2  25908  colmid  26476  outpasch  26543  lmiisolem  26584  elpreq  30292  fzne1  30513  esumcvgre  31352  ballotlem2  31748  lclkrlem2h  38652  aomclem5  39665  cvgdvgrat  40652  bccbc  40684  elunnel2  41303  stoweidlem26  42318  stoweidlem34  42326  fourierswlem  42522