Theorem orcanai 1001

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∨ wo 845

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 397  df-or 846

This theorem is referenced by:  elunnel1  4148  elunnel2  4149  bren2  8975  php  9206  phpOLD  9218  unxpdomlem3  9248  tcrank  9875  dfac12lem1  10134  dfac12lem2  10135  ttukeylem3  10502  ttukeylem5  10504  ttukeylem6  10505  xrmax2  13151  xrmin1  13152  xrge0nre  13426  ccatco  14782  pcgcd  16807  mreexexd  17588  tsrlemax  18535  gsumval2  18601  xrsdsreval  20982  xrsdsreclb  20984  xrsxmet  24316  elii2  24443  xrhmeo  24453  pcoass  24531  limccnp  25399  logreclem  26256  eldmgm  26515  lgsdir2  26822  maxs2  27258  mins1  27259  colmid  27928  outpasch  27995  lmiisolem  28036  elpreq  31754  fzne1  31986  esumcvgre  33077  ballotlem2  33475  lclkrlem2h  40373  aomclem5  41785  cvgdvgrat  43057  bccbc  43089  stoweidlem26  44728  stoweidlem34  44736  fourierswlem  44932