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  4117  elunnel2  4118  bren2  8954  php  9171  unxpdomlem3  9199  tcrank  9837  dfac12lem1  10097  dfac12lem2  10098  ttukeylem3  10464  ttukeylem5  10466  ttukeylem6  10467  xrmax2  13136  xrmin1  13137  xrge0nre  13414  fzne1  13565  ccatco  14801  pcgcd  16849  mreexexd  17609  tsrlemax  18545  gsumval2  18613  xrsdsreval  21328  xrsdsreclb  21330  xrsxmet  24698  elii2  24832  xrhmeo  24844  pcoass  24924  limccnp  25792  logreclem  26672  eldmgm  26932  lgsdir2  27241  maxs2  27678  mins1  27679  colmid  28615  outpasch  28682  lmiisolem  28723  elpreq  32457  2exple2exp  32770  irredminply  33706  esumcvgre  34081  ballotlem2  34480  lclkrlem2h  41508  aomclem5  43047  cvgdvgrat  44302  bccbc  44334  stoweidlem26  46024  stoweidlem34  46032  fourierswlem  46228