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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   ∨ wo 860

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

This theorem is referenced by:  elunnel1  4110  elunnel2  4111  bren2  8968  php  9179  unxpdomlem3  9206  tcrank  9844  dfac12lem1  10115  dfac12lem2  10116  ttukeylem3  10483  ttukeylem5  10485  ttukeylem6  10486  xrmax2  13193  xrmin1  13194  xrge0nre  13471  fzne1  13623  ccatco  14862  pcgcd  16928  mreexexd  17694  tsrlemax  18632  gsumval2  18734  xrsdsreval  21522  xrsdsreclb  21524  xrsxmet  24928  elii2  25056  xrhmeo  25066  pcoass  25144  limccnp  26011  logreclem  26885  eldmgm  27144  lgsdir2  27452  maxs2  27892  mins1  27893  colmid  28919  outpasch  28986  lmiisolem  29048  elpreq  32784  2exple2exp  33091  irredminply  34023  esumcvgre  34398  ballotlem2  34796  lclkrlem2h  42150  aomclem5  43647  cvgdvgrat  44887  bccbc  44919  stoweidlem26  46598  stoweidlem34  46606  fourierswlem  46802