Theorem orcanai 950

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

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 382   ∧ wa 383

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 196  df-or 384  df-an 385

This theorem is referenced by:  elunnel1  3716  bren2  7872  php  8029  unxpdomlem3  8051  tcrank  8630  dfac12lem1  8848  dfac12lem2  8849  ttukeylem3  9216  ttukeylem5  9218  ttukeylem6  9219  xrmax2  11881  xrmin1  11882  xrge0nre  12148  ccatco  13432  pcgcd  15420  mreexexd  16131  tsrlemax  17043  gsumval2  17103  xrsdsreval  19610  xrsdsreclb  19612  xrsxmet  22420  elii2  22543  xrhmeo  22553  pcoass  22632  limccnp  23461  logreclem  24300  eldmgm  24548  lgsdir2  24855  colmid  25383  lmiisolem  25488  elpreq  28744  esumcvgre  29480  eulerpartlemgvv  29765  ballotlem2  29877  nofulllem5  31105  lclkrlem2h  35821  aomclem5  36646  cvgdvgrat  37534  bccbc  37566  elunnel2  38221  stoweidlem26  38919  stoweidlem34  38927  fourierswlem  39123