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

Theorem orcanai 952
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 392 . 2 (𝜑 → (¬ 𝜓𝜒))
32imp 445 1 ((𝜑 ∧ ¬ 𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 383  wa 384
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 197  df-or 385  df-an 386
This theorem is referenced by:  elunnel1  3752  bren2  7983  php  8141  unxpdomlem3  8163  tcrank  8744  dfac12lem1  8962  dfac12lem2  8963  ttukeylem3  9330  ttukeylem5  9332  ttukeylem6  9333  xrmax2  12004  xrmin1  12005  xrge0nre  12274  ccatco  13575  pcgcd  15576  mreexexd  16302  tsrlemax  17214  gsumval2  17274  xrsdsreval  19785  xrsdsreclb  19787  xrsxmet  22606  elii2  22729  xrhmeo  22739  pcoass  22818  limccnp  23649  logreclem  24494  eldmgm  24742  lgsdir2  25049  colmid  25577  lmiisolem  25682  elpreq  29344  esumcvgre  30138  eulerpartlemgvv  30423  ballotlem2  30535  lclkrlem2h  36629  aomclem5  37454  cvgdvgrat  38338  bccbc  38370  elunnel2  39024  stoweidlem26  40012  stoweidlem34  40020  fourierswlem  40216
  Copyright terms: Public domain W3C validator