Theorem orcanai 999

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

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

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 206  df-an 396  df-or 844

This theorem is referenced by:  elunnel1  4088  bren2  8742  php  8957  phpOLD  8970  unxpdomlem3  8990  tcrank  9626  dfac12lem1  9883  dfac12lem2  9884  ttukeylem3  10251  ttukeylem5  10253  ttukeylem6  10254  xrmax2  12892  xrmin1  12893  xrge0nre  13167  ccatco  14529  pcgcd  16560  mreexexd  17338  tsrlemax  18285  gsumval2  18351  xrsdsreval  20624  xrsdsreclb  20626  xrsxmet  23953  elii2  24080  xrhmeo  24090  pcoass  24168  limccnp  25036  logreclem  25893  eldmgm  26152  lgsdir2  26459  colmid  27030  outpasch  27097  lmiisolem  27138  elpreq  30857  fzne1  31088  esumcvgre  32038  ballotlem2  32434  lclkrlem2h  39507  aomclem5  40863  cvgdvgrat  41884  bccbc  41916  elunnel2  42535  stoweidlem26  43521  stoweidlem34  43529  fourierswlem  43725