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

Theorem orcanai 999
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 861 . 2 (𝜑 → (¬ 𝜓𝜒))
32imp 406 1 ((𝜑 ∧ ¬ 𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  wo 844
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 206  df-an 396  df-or 845
This theorem is referenced by:  elunnel1  4141  elunnel2  4142  bren2  8974  php  9205  phpOLD  9217  unxpdomlem3  9247  tcrank  9874  dfac12lem1  10133  dfac12lem2  10134  ttukeylem3  10501  ttukeylem5  10503  ttukeylem6  10504  xrmax2  13151  xrmin1  13152  xrge0nre  13426  ccatco  14782  pcgcd  16807  mreexexd  17588  tsrlemax  18538  gsumval2  18606  xrsdsreval  21269  xrsdsreclb  21271  xrsxmet  24635  elii2  24769  xrhmeo  24781  pcoass  24861  limccnp  25730  logreclem  26598  eldmgm  26858  lgsdir2  27167  maxs2  27603  mins1  27604  colmid  28363  outpasch  28430  lmiisolem  28471  elpreq  32191  fzne1  32423  esumcvgre  33544  ballotlem2  33942  lclkrlem2h  40841  aomclem5  42255  cvgdvgrat  43527  bccbc  43559  stoweidlem26  45193  stoweidlem34  45201  fourierswlem  45397
  Copyright terms: Public domain W3C validator