MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  orcanai Structured version   Visualization version   GIF version

Theorem orcanai 996
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
StepHypRef Expression
1 orcanai.1 . . 3 (𝜑 → (𝜓𝜒))
21ord 858 . 2 (𝜑 → (¬ 𝜓𝜒))
32imp 407 1 ((𝜑 ∧ ¬ 𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  wo 841
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 842
This theorem is referenced by:  elunnel1  4123  bren2  8528  php  8689  unxpdomlem3  8712  tcrank  9301  dfac12lem1  9557  dfac12lem2  9558  ttukeylem3  9921  ttukeylem5  9923  ttukeylem6  9924  xrmax2  12557  xrmin1  12558  xrge0nre  12829  ccatco  14185  pcgcd  16202  mreexexd  16907  tsrlemax  17818  gsumval2  17884  xrsdsreval  20518  xrsdsreclb  20520  xrsxmet  23344  elii2  23467  xrhmeo  23477  pcoass  23555  limccnp  24416  logreclem  25267  eldmgm  25526  lgsdir2  25833  colmid  26401  outpasch  26468  lmiisolem  26509  elpreq  30217  fzne1  30437  esumcvgre  31249  ballotlem2  31645  lclkrlem2h  38530  aomclem5  39536  cvgdvgrat  40522  bccbc  40554  elunnel2  41173  stoweidlem26  42188  stoweidlem34  42196  fourierswlem  42392
  Copyright terms: Public domain W3C validator