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  4120  elunnel2  4121  bren2  8957  php  9177  unxpdomlem3  9206  tcrank  9844  dfac12lem1  10104  dfac12lem2  10105  ttukeylem3  10471  ttukeylem5  10473  ttukeylem6  10474  xrmax2  13143  xrmin1  13144  xrge0nre  13421  fzne1  13572  ccatco  14808  pcgcd  16856  mreexexd  17616  tsrlemax  18552  gsumval2  18620  xrsdsreval  21335  xrsdsreclb  21337  xrsxmet  24705  elii2  24839  xrhmeo  24851  pcoass  24931  limccnp  25799  logreclem  26679  eldmgm  26939  lgsdir2  27248  maxs2  27685  mins1  27686  colmid  28622  outpasch  28689  lmiisolem  28730  elpreq  32464  2exple2exp  32777  irredminply  33713  esumcvgre  34088  ballotlem2  34487  lclkrlem2h  41515  aomclem5  43054  cvgdvgrat  44309  bccbc  44341  stoweidlem26  46031  stoweidlem34  46039  fourierswlem  46235