Theorem orcanai 999

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

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

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 206  df-an 396  df-or 845

This theorem is referenced by:  elunnel1  4141  elunnel2  4142  bren2  8974  php  9205  phpOLD  9217  unxpdomlem3  9247  tcrank  9874  dfac12lem1  10133  dfac12lem2  10134  ttukeylem3  10501  ttukeylem5  10503  ttukeylem6  10504  xrmax2  13151  xrmin1  13152  xrge0nre  13426  ccatco  14782  pcgcd  16807  mreexexd  17588  tsrlemax  18538  gsumval2  18606  xrsdsreval  21269  xrsdsreclb  21271  xrsxmet  24635  elii2  24769  xrhmeo  24781  pcoass  24861  limccnp  25730  logreclem  26598  eldmgm  26858  lgsdir2  27167  maxs2  27603  mins1  27604  colmid  28363  outpasch  28430  lmiisolem  28471  elpreq  32191  fzne1  32423  esumcvgre  33544  ballotlem2  33942  lclkrlem2h  40841  aomclem5  42255  cvgdvgrat  43527  bccbc  43559  stoweidlem26  45193  stoweidlem34  45201  fourierswlem  45397