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  4102  elunnel2  4103  bren2  8900  php  9111  unxpdomlem3  9137  tcrank  9769  dfac12lem1  10027  dfac12lem2  10028  ttukeylem3  10394  ttukeylem5  10396  ttukeylem6  10397  xrmax2  13067  xrmin1  13068  xrge0nre  13345  fzne1  13496  ccatco  14734  pcgcd  16782  mreexexd  17546  tsrlemax  18484  gsumval2  18586  xrsdsreval  21341  xrsdsreclb  21343  xrsxmet  24718  elii2  24852  xrhmeo  24864  pcoass  24944  limccnp  25812  logreclem  26692  eldmgm  26952  lgsdir2  27261  maxs2  27698  mins1  27699  colmid  28659  outpasch  28726  lmiisolem  28767  elpreq  32498  2exple2exp  32818  irredminply  33719  esumcvgre  34094  ballotlem2  34492  lclkrlem2h  41532  aomclem5  43070  cvgdvgrat  44325  bccbc  44357  stoweidlem26  46043  stoweidlem34  46051  fourierswlem  46247