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  4107  elunnel2  4108  bren2  8979  php  9190  unxpdomlem3  9217  tcrank  9855  dfac12lem1  10126  dfac12lem2  10127  ttukeylem3  10494  ttukeylem5  10496  ttukeylem6  10497  xrmax2  13201  xrmin1  13202  xrge0nre  13479  fzne1  13632  ccatco  14872  pcgcd  16937  mreexexd  17703  tsrlemax  18641  gsumval2  18743  xrsdsreval  21541  xrsdsreclb  21543  xrsxmet  24946  elii2  25074  xrhmeo  25084  pcoass  25162  limccnp  26029  logreclem  26903  eldmgm  27162  lgsdir2  27470  maxs2  27910  mins1  27911  colmid  28941  outpasch  29012  lmiisolem  29079  elpreq  32840  2exple2exp  33144  irredminply  34072  esumcvgre  34447  ballotlem2  34845  nmulel1  36658  lclkrlem2h  42256  aomclem5  43755  cvgdvgrat  44993  bccbc  45025  stoweidlem26  46710  stoweidlem34  46718  fourierswlem  46914