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

Theorem orcanai 998
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 860 . 2 (𝜑 → (¬ 𝜓𝜒))
32imp 407 1 ((𝜑 ∧ ¬ 𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  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 208  df-an 397  df-or 844
This theorem is referenced by:  elunnel1  4129  bren2  8532  php  8693  unxpdomlem3  8716  tcrank  9305  dfac12lem1  9561  dfac12lem2  9562  ttukeylem3  9925  ttukeylem5  9927  ttukeylem6  9928  xrmax2  12562  xrmin1  12563  xrge0nre  12834  ccatco  14190  pcgcd  16206  mreexexd  16911  tsrlemax  17822  gsumval2  17887  xrsdsreval  20506  xrsdsreclb  20508  xrsxmet  23332  elii2  23455  xrhmeo  23465  pcoass  23543  limccnp  24404  logreclem  25253  eldmgm  25513  lgsdir2  25820  colmid  26388  outpasch  26455  lmiisolem  26496  elpreq  30205  fzne1  30425  esumcvgre  31237  ballotlem2  31633  lclkrlem2h  38518  aomclem5  39520  cvgdvgrat  40507  bccbc  40539  elunnel2  41158  stoweidlem26  42174  stoweidlem34  42182  fourierswlem  42378
  Copyright terms: Public domain W3C validator