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  4107  elunnel2  4108  bren2  8924  php  9135  unxpdomlem3  9162  tcrank  9800  dfac12lem1  10058  dfac12lem2  10059  ttukeylem3  10425  ttukeylem5  10427  ttukeylem6  10428  xrmax2  13095  xrmin1  13096  xrge0nre  13373  fzne1  13524  ccatco  14762  pcgcd  16810  mreexexd  17575  tsrlemax  18513  gsumval2  18615  xrsdsreval  21370  xrsdsreclb  21372  xrsxmet  24758  elii2  24892  xrhmeo  24904  pcoass  24984  limccnp  25852  logreclem  26732  eldmgm  26992  lgsdir2  27301  maxs2  27742  mins1  27743  colmid  28743  outpasch  28810  lmiisolem  28851  elpreq  32585  2exple2exp  32907  irredminply  33854  esumcvgre  34229  ballotlem2  34627  lclkrlem2h  41811  aomclem5  43336  cvgdvgrat  44590  bccbc  44622  stoweidlem26  46306  stoweidlem34  46314  fourierswlem  46510