Theorem orcanai 1017

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

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

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 401  df-or 861

This theorem is used by:  elunnel1  4107  elunnel2  4108  bren2  8978  php  9189  unxpdomlem3  9216  tcrank  9854  dfac12lem1  10134  dfac12lem2  10135  ttukeylem3  10501  ttukeylem5  10503  ttukeylem6  10504  xrmax2  13208  xrmin1  13209  xrge0nre  13486  fzne1  13639  ccatco  14879  pcgcd  16944  mreexexd  17710  tsrlemax  18648  gsumval2  18750  xrsdsreval  21573  xrsdsreclb  21575  xrsxmet  24978  elii2  25106  xrhmeo  25116  pcoass  25194  limccnp  26061  logreclem  26938  eldmgm  27197  lgsdir2  27505  maxs2  27945  mins1  27946  colmid  28976  outpasch  29048  lmiisolem  29116  elpreq  32885  2exple2exp  33189  irredminply  34115  esumcvgre  34490  ballotlem2  34888  nmulel1  36715  lclkrlem2h  42316  aomclem5  43813  cvgdvgrat  45051  bccbc  45083  stoweidlem26  46768  stoweidlem34  46776  fourierswlem  46972