Theorem orcanai 1003

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

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

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 847

This theorem is referenced by:  elunnel1  4177  elunnel2  4178  bren2  9043  php  9273  phpOLD  9285  unxpdomlem3  9315  tcrank  9953  dfac12lem1  10213  dfac12lem2  10214  ttukeylem3  10580  ttukeylem5  10582  ttukeylem6  10583  xrmax2  13238  xrmin1  13239  xrge0nre  13513  ccatco  14884  pcgcd  16925  mreexexd  17706  tsrlemax  18656  gsumval2  18724  xrsdsreval  21452  xrsdsreclb  21454  xrsxmet  24850  elii2  24984  xrhmeo  24996  pcoass  25076  limccnp  25946  logreclem  26823  eldmgm  27083  lgsdir2  27392  maxs2  27829  mins1  27830  colmid  28714  outpasch  28781  lmiisolem  28822  elpreq  32558  fzne1  32793  irredminply  33707  esumcvgre  34055  ballotlem2  34453  lclkrlem2h  41471  aomclem5  43015  cvgdvgrat  44282  bccbc  44314  stoweidlem26  45947  stoweidlem34  45955  fourierswlem  46151