Theorem orcanai 1032

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 386   ∨ wo 880

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 199  df-an 387  df-or 881

This theorem is referenced by:  elunnel1  3980  bren2  8252  php  8412  unxpdomlem3  8434  tcrank  9023  dfac12lem1  9279  dfac12lem2  9280  ttukeylem3  9647  ttukeylem5  9649  ttukeylem6  9650  xrmax2  12294  xrmin1  12295  xrge0nre  12566  ccatco  13955  pcgcd  15952  mreexexd  16660  tsrlemax  17572  gsumval2  17632  xrsdsreval  20150  xrsdsreclb  20152  xrsxmet  22981  elii2  23104  xrhmeo  23114  pcoass  23192  limccnp  24053  logreclem  24901  eldmgm  25160  lgsdir2  25467  colmid  25999  lmiisolem  26104  elpreq  29907  esumcvgre  30697  eulerpartlemgvv  30982  ballotlem2  31095  lclkrlem2h  37588  aomclem5  38470  cvgdvgrat  39351  bccbc  39383  elunnel2  40015  stoweidlem26  41036  stoweidlem34  41044  fourierswlem  41240