Theorem orcanai 1005

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

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

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 849

This theorem is referenced by:  elunnel1  4095  elunnel2  4096  bren2  8930  php  9141  unxpdomlem3  9168  tcrank  9808  dfac12lem1  10066  dfac12lem2  10067  ttukeylem3  10433  ttukeylem5  10435  ttukeylem6  10436  xrmax2  13128  xrmin1  13129  xrge0nre  13406  fzne1  13558  ccatco  14797  pcgcd  16849  mreexexd  17614  tsrlemax  18552  gsumval2  18654  xrsdsreval  21392  xrsdsreclb  21394  xrsxmet  24775  elii2  24903  xrhmeo  24913  pcoass  24991  limccnp  25858  logreclem  26726  eldmgm  26985  lgsdir2  27293  maxs2  27734  mins1  27735  colmid  28756  outpasch  28823  lmiisolem  28864  elpreq  32598  2exple2exp  32918  irredminply  33860  esumcvgre  34235  ballotlem2  34633  lclkrlem2h  41960  aomclem5  43486  cvgdvgrat  44740  bccbc  44772  stoweidlem26  46454  stoweidlem34  46462  fourierswlem  46658