Theorem orcanai 1000

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∨ 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 210  df-an 400  df-or 845

This theorem is referenced by:  elunnel1  4077  bren2  8523  php  8685  unxpdomlem3  8708  tcrank  9297  dfac12lem1  9554  dfac12lem2  9555  ttukeylem3  9922  ttukeylem5  9924  ttukeylem6  9925  xrmax2  12557  xrmin1  12558  xrge0nre  12831  ccatco  14188  pcgcd  16204  mreexexd  16911  tsrlemax  17822  gsumval2  17888  xrsdsreval  20136  xrsdsreclb  20138  xrsxmet  23414  elii2  23541  xrhmeo  23551  pcoass  23629  limccnp  24494  logreclem  25348  eldmgm  25607  lgsdir2  25914  colmid  26482  outpasch  26549  lmiisolem  26590  elpreq  30302  fzne1  30537  esumcvgre  31460  ballotlem2  31856  lclkrlem2h  38810  aomclem5  40002  cvgdvgrat  41017  bccbc  41049  elunnel2  41668  stoweidlem26  42668  stoweidlem34  42676  fourierswlem  42872