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  4107  elunnel2  4108  bren2  8915  php  9131  unxpdomlem3  9157  tcrank  9799  dfac12lem1  10057  dfac12lem2  10058  ttukeylem3  10424  ttukeylem5  10426  ttukeylem6  10427  xrmax2  13096  xrmin1  13097  xrge0nre  13374  fzne1  13525  ccatco  14760  pcgcd  16808  mreexexd  17572  tsrlemax  18510  gsumval2  18578  xrsdsreval  21336  xrsdsreclb  21338  xrsxmet  24714  elii2  24848  xrhmeo  24860  pcoass  24940  limccnp  25808  logreclem  26688  eldmgm  26948  lgsdir2  27257  maxs2  27694  mins1  27695  colmid  28651  outpasch  28718  lmiisolem  28759  elpreq  32490  2exple2exp  32803  irredminply  33682  esumcvgre  34057  ballotlem2  34456  lclkrlem2h  41493  aomclem5  43031  cvgdvgrat  44286  bccbc  44318  stoweidlem26  46008  stoweidlem34  46016  fourierswlem  46212