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 408	1 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397   ∨ 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 398  df-or 846

This theorem is referenced by:  elunnel1  4090  bren2  8804  php  9031  phpOLD  9043  unxpdomlem3  9073  tcrank  9686  dfac12lem1  9945  dfac12lem2  9946  ttukeylem3  10313  ttukeylem5  10315  ttukeylem6  10316  xrmax2  12956  xrmin1  12957  xrge0nre  13231  ccatco  14593  pcgcd  16624  mreexexd  17402  tsrlemax  18349  gsumval2  18415  xrsdsreval  20688  xrsdsreclb  20690  xrsxmet  24017  elii2  24144  xrhmeo  24154  pcoass  24232  limccnp  25100  logreclem  25957  eldmgm  26216  lgsdir2  26523  colmid  27094  outpasch  27161  lmiisolem  27202  elpreq  30923  fzne1  31154  esumcvgre  32104  ballotlem2  32500  lclkrlem2h  39570  aomclem5  40921  cvgdvgrat  41969  bccbc  42001  elunnel2  42620  stoweidlem26  43616  stoweidlem34  43624  fourierswlem  43820