Theorem orcanai 1004

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

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

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 848

This theorem is referenced by:  elunnel1  4129  elunnel2  4130  bren2  8997  php  9221  phpOLD  9231  unxpdomlem3  9260  tcrank  9898  dfac12lem1  10158  dfac12lem2  10159  ttukeylem3  10525  ttukeylem5  10527  ttukeylem6  10528  xrmax2  13192  xrmin1  13193  xrge0nre  13470  fzne1  13621  ccatco  14854  pcgcd  16898  mreexexd  17660  tsrlemax  18596  gsumval2  18664  xrsdsreval  21379  xrsdsreclb  21381  xrsxmet  24749  elii2  24883  xrhmeo  24895  pcoass  24975  limccnp  25844  logreclem  26724  eldmgm  26984  lgsdir2  27293  maxs2  27730  mins1  27731  colmid  28667  outpasch  28734  lmiisolem  28775  elpreq  32509  2exple2exp  32824  irredminply  33750  esumcvgre  34122  ballotlem2  34521  lclkrlem2h  41533  aomclem5  43082  cvgdvgrat  44337  bccbc  44369  stoweidlem26  46055  stoweidlem34  46063  fourierswlem  46259