Theorem orcanai 1004

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

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

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 848

This theorem is referenced by:  elunnel1  4129  elunnel2  4130  bren2  8995  php  9219  phpOLD  9229  unxpdomlem3  9258  tcrank  9896  dfac12lem1  10156  dfac12lem2  10157  ttukeylem3  10523  ttukeylem5  10525  ttukeylem6  10526  xrmax2  13190  xrmin1  13191  xrge0nre  13468  fzne1  13619  ccatco  14852  pcgcd  16896  mreexexd  17658  tsrlemax  18594  gsumval2  18662  xrsdsreval  21377  xrsdsreclb  21379  xrsxmet  24747  elii2  24881  xrhmeo  24893  pcoass  24973  limccnp  25842  logreclem  26722  eldmgm  26982  lgsdir2  27291  maxs2  27728  mins1  27729  colmid  28613  outpasch  28680  lmiisolem  28721  elpreq  32455  2exple2exp  32770  irredminply  33696  esumcvgre  34068  ballotlem2  34467  lclkrlem2h  41479  aomclem5  43029  cvgdvgrat  44285  bccbc  44317  stoweidlem26  46003  stoweidlem34  46011  fourierswlem  46207