Theorem orcanai 1018

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862

This theorem is used by:  elunnel1  4104  elunnel2  4105  bren2  8992  php  9204  unxpdomlem3  9231  tcrank  9869  dfac12lem1  10149  dfac12lem2  10150  ttukeylem3  10516  ttukeylem5  10518  ttukeylem6  10519  xrmax2  13230  xrmin1  13231  xrge0nre  13508  fzne1  13661  ccatco  14908  pcgcd  16974  mreexexd  17740  tsrlemax  18678  gsumval2  18792  xrsdsreval  21629  xrsdsreclb  21631  xrsxmet  25040  elii2  25168  xrhmeo  25178  pcoass  25256  limccnp  26123  logreclem  27000  eldmgm  27259  lgsdir2  27567  maxs2  28007  mins1  28008  colmid  29040  outpasch  29113  lmiisolem  29181  elpreq  33004  2exple2exp  33306  irredminply  34228  esumcvgre  34603  ballotlem2  35002  nmulel1  36797  lclkrlem2h  42389  aomclem5  43901  cvgdvgrat  45139  bccbc  45171  stoweidlem26  46856  stoweidlem34  46864  fourierswlem  47060