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  4105  elunnel2  4106  bren2  8915  php  9126  unxpdomlem3  9152  tcrank  9787  dfac12lem1  10045  dfac12lem2  10046  ttukeylem3  10412  ttukeylem5  10414  ttukeylem6  10415  xrmax2  13085  xrmin1  13086  xrge0nre  13363  fzne1  13514  ccatco  14752  pcgcd  16800  mreexexd  17564  tsrlemax  18502  gsumval2  18604  xrsdsreval  21358  xrsdsreclb  21360  xrsxmet  24735  elii2  24869  xrhmeo  24881  pcoass  24961  limccnp  25829  logreclem  26709  eldmgm  26969  lgsdir2  27278  maxs2  27715  mins1  27716  colmid  28676  outpasch  28743  lmiisolem  28784  elpreq  32519  2exple2exp  32839  irredminply  33740  esumcvgre  34115  ballotlem2  34513  lclkrlem2h  41623  aomclem5  43165  cvgdvgrat  44420  bccbc  44452  stoweidlem26  46138  stoweidlem34  46146  fourierswlem  46342