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  27939  outpasch  28006  lmiisolem  28047  elpreq  31767  fzne1  31999  esumcvgre  33089  ballotlem2  33487  lclkrlem2h  40385  aomclem5  41800  cvgdvgrat  43072  bccbc  43104  stoweidlem26  44742  stoweidlem34  44750  fourierswlem  44946