Theorem orcanai 952

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

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 383   ∧ wa 384

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 197  df-or 385  df-an 386

This theorem is referenced by:  elunnel1  3754  bren2  7986  php  8144  unxpdomlem3  8166  tcrank  8747  dfac12lem1  8965  dfac12lem2  8966  ttukeylem3  9333  ttukeylem5  9335  ttukeylem6  9336  xrmax2  12007  xrmin1  12008  xrge0nre  12277  ccatco  13581  pcgcd  15582  mreexexd  16308  tsrlemax  17220  gsumval2  17280  xrsdsreval  19791  xrsdsreclb  19793  xrsxmet  22612  elii2  22735  xrhmeo  22745  pcoass  22824  limccnp  23655  logreclem  24500  eldmgm  24748  lgsdir2  25055  colmid  25583  lmiisolem  25688  elpreq  29360  esumcvgre  30153  eulerpartlemgvv  30438  ballotlem2  30550  lclkrlem2h  36803  aomclem5  37628  cvgdvgrat  38512  bccbc  38544  elunnel2  39198  stoweidlem26  40243  stoweidlem34  40251  fourierswlem  40447