Theorem orcanai 1010

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∨ wo 853

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 208  df-an 397  df-or 854

This theorem is referenced by:  elunnel1  4091  elunnel2  4092  bren2  8927  php  9138  unxpdomlem3  9165  tcrank  9806  dfac12lem1  10064  dfac12lem2  10065  ttukeylem3  10431  ttukeylem5  10433  ttukeylem6  10434  xrmax2  13126  xrmin1  13127  xrge0nre  13404  fzne1  13556  ccatco  14795  pcgcd  16847  mreexexd  17612  tsrlemax  18550  gsumval2  18652  xrsdsreval  21394  xrsdsreclb  21396  xrsxmet  24800  elii2  24928  xrhmeo  24938  pcoass  25016  limccnp  25883  logreclem  26751  eldmgm  27010  lgsdir2  27318  maxs2  27759  mins1  27760  colmid  28781  outpasch  28848  lmiisolem  28889  elpreq  32623  2exple2exp  32944  irredminply  33907  esumcvgre  34282  ballotlem2  34680  lclkrlem2h  42007  aomclem5  43504  cvgdvgrat  44758  bccbc  44790  stoweidlem26  46470  stoweidlem34  46478  fourierswlem  46674