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

Theorem orcanai 1000
 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 410 1 ((𝜑 ∧ ¬ 𝜓) → 𝜒)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∨ 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 210  df-an 400  df-or 845 This theorem is referenced by:  elunnel1  4055  bren2  8558  php  8723  unxpdomlem3  8762  tcrank  9346  dfac12lem1  9603  dfac12lem2  9604  ttukeylem3  9971  ttukeylem5  9973  ttukeylem6  9974  xrmax2  12610  xrmin1  12611  xrge0nre  12885  ccatco  14244  pcgcd  16269  mreexexd  16977  tsrlemax  17896  gsumval2  17962  xrsdsreval  20211  xrsdsreclb  20213  xrsxmet  23510  elii2  23637  xrhmeo  23647  pcoass  23725  limccnp  24590  logreclem  25447  eldmgm  25706  lgsdir2  26013  colmid  26581  outpasch  26648  lmiisolem  26689  elpreq  30400  fzne1  30633  esumcvgre  31578  ballotlem2  31974  lclkrlem2h  39112  aomclem5  40397  cvgdvgrat  41412  bccbc  41444  elunnel2  42063  stoweidlem26  43056  stoweidlem34  43064  fourierswlem  43260
 Copyright terms: Public domain W3C validator