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

Theorem orcanai 990
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 391 . 2 (𝜑 → (¬ 𝜓𝜒))
32imp 444 1 ((𝜑 ∧ ¬ 𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 382  wa 383
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 384  df-an 385
This theorem is referenced by:  elunnel1  3898  bren2  8155  php  8312  unxpdomlem3  8334  tcrank  8923  dfac12lem1  9178  dfac12lem2  9179  ttukeylem3  9546  ttukeylem5  9548  ttukeylem6  9549  xrmax2  12221  xrmin1  12222  xrge0nre  12491  ccatco  13802  pcgcd  15805  mreexexd  16531  tsrlemax  17442  gsumval2  17502  xrsdsreval  20014  xrsdsreclb  20016  xrsxmet  22834  elii2  22957  xrhmeo  22967  pcoass  23045  limccnp  23875  logreclem  24721  eldmgm  24969  lgsdir2  25276  colmid  25804  lmiisolem  25909  elpreq  29689  esumcvgre  30484  eulerpartlemgvv  30769  ballotlem2  30881  lclkrlem2h  37324  aomclem5  38149  cvgdvgrat  39033  bccbc  39065  elunnel2  39716  stoweidlem26  40765  stoweidlem34  40773  fourierswlem  40969
  Copyright terms: Public domain W3C validator