Theorem orcanai 1002

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 408	1 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397   ∨ 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 206  df-an 398  df-or 847

This theorem is referenced by:  elunnel1  4150  elunnel2  4151  bren2  8979  php  9210  phpOLD  9222  unxpdomlem3  9252  tcrank  9879  dfac12lem1  10138  dfac12lem2  10139  ttukeylem3  10506  ttukeylem5  10508  ttukeylem6  10509  xrmax2  13155  xrmin1  13156  xrge0nre  13430  ccatco  14786  pcgcd  16811  mreexexd  17592  tsrlemax  18539  gsumval2  18605  xrsdsreval  20990  xrsdsreclb  20992  xrsxmet  24325  elii2  24452  xrhmeo  24462  pcoass  24540  limccnp  25408  logreclem  26267  eldmgm  26526  lgsdir2  26833  maxs2  27269  mins1  27270  colmid  27970  outpasch  28037  lmiisolem  28078  elpreq  31798  fzne1  32030  esumcvgre  33120  ballotlem2  33518  lclkrlem2h  40433  aomclem5  41848  cvgdvgrat  43120  bccbc  43152  stoweidlem26  44790  stoweidlem34  44798  fourierswlem  44994