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  4108  elunnel2  4109  bren2  8932  php  9143  unxpdomlem3  9170  tcrank  9808  dfac12lem1  10066  dfac12lem2  10067  ttukeylem3  10433  ttukeylem5  10435  ttukeylem6  10436  xrmax2  13103  xrmin1  13104  xrge0nre  13381  fzne1  13532  ccatco  14770  pcgcd  16818  mreexexd  17583  tsrlemax  18521  gsumval2  18623  xrsdsreval  21378  xrsdsreclb  21380  xrsxmet  24766  elii2  24900  xrhmeo  24912  pcoass  24992  limccnp  25860  logreclem  26740  eldmgm  27000  lgsdir2  27309  maxs2  27750  mins1  27751  colmid  28772  outpasch  28839  lmiisolem  28880  elpreq  32614  2exple2exp  32936  irredminply  33893  esumcvgre  34268  ballotlem2  34666  lclkrlem2h  41879  aomclem5  43404  cvgdvgrat  44658  bccbc  44690  stoweidlem26  46373  stoweidlem34  46381  fourierswlem  46577