Theorem orcanai 1004

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 847

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 848

This theorem is referenced by:  elunnel1  4163  elunnel2  4164  bren2  9021  php  9244  phpOLD  9256  unxpdomlem3  9285  tcrank  9921  dfac12lem1  10181  dfac12lem2  10182  ttukeylem3  10548  ttukeylem5  10550  ttukeylem6  10551  xrmax2  13214  xrmin1  13215  xrge0nre  13489  fzne1  13640  ccatco  14870  pcgcd  16911  mreexexd  17692  tsrlemax  18643  gsumval2  18711  xrsdsreval  21446  xrsdsreclb  21448  xrsxmet  24844  elii2  24978  xrhmeo  24990  pcoass  25070  limccnp  25940  logreclem  26819  eldmgm  27079  lgsdir2  27388  maxs2  27825  mins1  27826  colmid  28710  outpasch  28777  lmiisolem  28818  elpreq  32555  irredminply  33721  esumcvgre  34071  ballotlem2  34469  lclkrlem2h  41496  aomclem5  43046  cvgdvgrat  44308  bccbc  44340  stoweidlem26  45981  stoweidlem34  45989  fourierswlem  46185