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

Theorem orcanai 1005
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 865 . 2 (𝜑 → (¬ 𝜓𝜒))
32imp 406 1 ((𝜑 ∧ ¬ 𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  wo 848
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 207  df-an 396  df-or 849
This theorem is referenced by:  elunnel1  4154  elunnel2  4155  bren2  9023  php  9247  phpOLD  9259  unxpdomlem3  9288  tcrank  9924  dfac12lem1  10184  dfac12lem2  10185  ttukeylem3  10551  ttukeylem5  10553  ttukeylem6  10554  xrmax2  13218  xrmin1  13219  xrge0nre  13493  fzne1  13644  ccatco  14874  pcgcd  16916  mreexexd  17691  tsrlemax  18631  gsumval2  18699  xrsdsreval  21429  xrsdsreclb  21431  xrsxmet  24831  elii2  24965  xrhmeo  24977  pcoass  25057  limccnp  25926  logreclem  26805  eldmgm  27065  lgsdir2  27374  maxs2  27811  mins1  27812  colmid  28696  outpasch  28763  lmiisolem  28804  elpreq  32548  2exple2exp  32834  irredminply  33757  esumcvgre  34092  ballotlem2  34491  lclkrlem2h  41516  aomclem5  43070  cvgdvgrat  44332  bccbc  44364  stoweidlem26  46041  stoweidlem34  46049  fourierswlem  46245
  Copyright terms: Public domain W3C validator