Theorem orcanai 1000

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∨ wo 844

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 210  df-an 400  df-or 845

This theorem is referenced by:  elunnel1  4055  bren2  8558  php  8723  unxpdomlem3  8762  tcrank  9346  dfac12lem1  9603  dfac12lem2  9604  ttukeylem3  9971  ttukeylem5  9973  ttukeylem6  9974  xrmax2  12610  xrmin1  12611  xrge0nre  12885  ccatco  14244  pcgcd  16269  mreexexd  16977  tsrlemax  17896  gsumval2  17962  xrsdsreval  20211  xrsdsreclb  20213  xrsxmet  23510  elii2  23637  xrhmeo  23647  pcoass  23725  limccnp  24590  logreclem  25447  eldmgm  25706  lgsdir2  26013  colmid  26581  outpasch  26648  lmiisolem  26689  elpreq  30400  fzne1  30633  esumcvgre  31578  ballotlem2  31974  lclkrlem2h  39112  aomclem5  40397  cvgdvgrat  41412  bccbc  41444  elunnel2  42063  stoweidlem26  43056  stoweidlem34  43064  fourierswlem  43260