Theorem orcanai 1013

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398   ∨ wo 856

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 209  df-an 399  df-or 857

This theorem is referenced by:  elunnel1  4102  elunnel2  4103  bren2  8953  php  9164  unxpdomlem3  9191  tcrank  9832  dfac12lem1  10090  dfac12lem2  10091  ttukeylem3  10458  ttukeylem5  10460  ttukeylem6  10461  xrmax2  13169  xrmin1  13170  xrge0nre  13447  fzne1  13599  ccatco  14838  pcgcd  16890  mreexexd  17656  tsrlemax  18594  gsumval2  18696  xrsdsreval  21437  xrsdsreclb  21439  xrsxmet  24843  elii2  24971  xrhmeo  24981  pcoass  25059  limccnp  25926  logreclem  26797  eldmgm  27056  lgsdir2  27364  maxs2  27804  mins1  27805  colmid  28827  outpasch  28894  lmiisolem  28935  elpreq  32669  2exple2exp  32990  irredminply  33967  esumcvgre  34342  ballotlem2  34740  lclkrlem2h  42086  aomclem5  43583  cvgdvgrat  44837  bccbc  44869  stoweidlem26  46548  stoweidlem34  46556  fourierswlem  46752