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  4156  elunnel2  4157  bren2  9038  php  9250  unxpdomlem3  9277  tcrank  9928  dfac12lem1  10249  dfac12lem2  10250  ttukeylem3  10616  ttukeylem5  10618  ttukeylem6  10619  xrmax2  13333  xrmin1  13334  xrge0nre  13611  fzne1  13765  ccatco  15014  pcgcd  17085  mreexexd  17851  tsrlemax  18789  gsumval2  18904  xrsdsreval  21748  xrsdsreclb  21750  xrsxmet  25159  elii2  25287  xrhmeo  25297  pcoass  25375  limccnp  26241  logreclem  27120  eldmgm  27379  lgsdir2  27687  maxs2  28157  mins1  28158  colmid  29190  outpasch  29263  lmiisolem  29331  elpreq  33196  2exple2exp  33495  irredminply  34418  esumcvgre  34793  ballotlem2  35191  onf1oracwevd  36052  nmulel1  37142  lclkrlem2h  42763  aomclem5  44253  cvgdvgrat  45489  bccbc  45521  stoweidlem26  47241  stoweidlem34  47249  fourierswlem  47445  parcoval2  50971