Theorem orcanai 1018

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862

This theorem is used by:  elunnel1  4153  elunnel2  4154  bren2  9011  php  9223  unxpdomlem3  9250  tcrank  9902  dfac12lem1  10223  dfac12lem2  10224  ttukeylem3  10590  ttukeylem5  10592  ttukeylem6  10593  xrmax2  13307  xrmin1  13308  xrge0nre  13585  fzne1  13739  ccatco  14987  pcgcd  17057  mreexexd  17823  tsrlemax  18761  gsumval2  18876  xrsdsreval  21719  xrsdsreclb  21721  xrsxmet  25130  elii2  25258  xrhmeo  25268  pcoass  25346  limccnp  26212  logreclem  27091  eldmgm  27350  lgsdir2  27658  maxs2  28128  mins1  28129  colmid  29161  outpasch  29234  lmiisolem  29302  elpreq  33167  2exple2exp  33468  irredminply  34391  esumcvgre  34766  ballotlem2  35164  onf1oracwevd  35964  nmulel1  37039  lclkrlem2h  42647  aomclem5  44136  cvgdvgrat  45373  bccbc  45405  stoweidlem26  47112  stoweidlem34  47120  fourierswlem  47316