Theorem orcanai 1005

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 848

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 207  df-an 396  df-or 849

This theorem is referenced by:  elunnel1  4095  elunnel2  4096  bren2  8921  php  9132  unxpdomlem3  9159  tcrank  9797  dfac12lem1  10055  dfac12lem2  10056  ttukeylem3  10422  ttukeylem5  10424  ttukeylem6  10425  xrmax2  13117  xrmin1  13118  xrge0nre  13395  fzne1  13547  ccatco  14786  pcgcd  16838  mreexexd  17603  tsrlemax  18541  gsumval2  18643  xrsdsreval  21399  xrsdsreclb  21401  xrsxmet  24784  elii2  24912  xrhmeo  24922  pcoass  25000  limccnp  25867  logreclem  26743  eldmgm  27003  lgsdir2  27312  maxs2  27753  mins1  27754  colmid  28775  outpasch  28842  lmiisolem  28883  elpreq  32618  2exple2exp  32938  irredminply  33881  esumcvgre  34256  ballotlem2  34654  lclkrlem2h  41971  aomclem5  43501  cvgdvgrat  44755  bccbc  44787  stoweidlem26  46469  stoweidlem34  46477  fourierswlem  46673