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

Theorem orcanai 1032
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 897 . 2 (𝜑 → (¬ 𝜓𝜒))
32imp 397 1 ((𝜑 ∧ ¬ 𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 386  wo 880
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 199  df-an 387  df-or 881
This theorem is referenced by:  elunnel1  3980  bren2  8252  php  8412  unxpdomlem3  8434  tcrank  9023  dfac12lem1  9279  dfac12lem2  9280  ttukeylem3  9647  ttukeylem5  9649  ttukeylem6  9650  xrmax2  12294  xrmin1  12295  xrge0nre  12566  ccatco  13955  pcgcd  15952  mreexexd  16660  tsrlemax  17572  gsumval2  17632  xrsdsreval  20150  xrsdsreclb  20152  xrsxmet  22981  elii2  23104  xrhmeo  23114  pcoass  23192  limccnp  24053  logreclem  24901  eldmgm  25160  lgsdir2  25467  colmid  25999  lmiisolem  26104  elpreq  29907  esumcvgre  30697  eulerpartlemgvv  30982  ballotlem2  31095  lclkrlem2h  37588  aomclem5  38470  cvgdvgrat  39351  bccbc  39383  elunnel2  40015  stoweidlem26  41036  stoweidlem34  41044  fourierswlem  41240
  Copyright terms: Public domain W3C validator