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  4100  elunnel2  4101  bren2  8988  php  9200  unxpdomlem3  9227  tcrank  9874  dfac12lem1  10194  dfac12lem2  10195  ttukeylem3  10561  ttukeylem5  10563  ttukeylem6  10564  xrmax2  13276  xrmin1  13277  xrge0nre  13554  fzne1  13707  ccatco  14954  pcgcd  17018  mreexexd  17784  tsrlemax  18722  gsumval2  18837  xrsdsreval  21680  xrsdsreclb  21682  xrsxmet  25091  elii2  25219  xrhmeo  25229  pcoass  25307  limccnp  26173  logreclem  27054  eldmgm  27313  lgsdir2  27621  maxs2  28061  mins1  28062  colmid  29094  outpasch  29167  lmiisolem  29235  elpreq  33058  2exple2exp  33359  irredminply  34282  esumcvgre  34657  ballotlem2  35056  nmulel1  36886  lclkrlem2h  42491  aomclem5  44003  cvgdvgrat  45241  bccbc  45273  stoweidlem26  46958  stoweidlem34  46966  fourierswlem  47162