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

Theorem orcanai 911
Description: Change disjunction in consequent to conjunction in antecedent. (Contributed by NM, 8-Jun-1994.)
Hypothesis
Ref Expression
orcanai.1  |-  ( ph  ->  ( ps  \/  ch ) )
Assertion
Ref Expression
orcanai  |-  ( (
ph  /\  -.  ps )  ->  ch )

Proof of Theorem orcanai
StepHypRef Expression
1 orcanai.1 . . 3  |-  ( ph  ->  ( ps  \/  ch ) )
21ord 375 . 2  |-  ( ph  ->  ( -.  ps  ->  ch ) )
32imp 427 1  |-  ( (
ph  /\  -.  ps )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 366    /\ wa 367
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 185  df-or 368  df-an 369
This theorem is referenced by:  bren2  7539  php  7694  unxpdomlem3  7719  tcrank  8293  dfac12lem1  8514  dfac12lem2  8515  ttukeylem3  8882  ttukeylem5  8884  ttukeylem6  8885  xrmax2  11380  xrmin1  11381  ccatco  12795  pcgcd  14488  tsrlemax  16052  gsumval2  16109  xrsdsreval  18661  xrsdsreclb  18663  xrsxmet  21483  elii2  21605  xrhmeo  21615  pcoass  21693  limccnp  22464  logreclem  23304  lgsdir2  23804  colmid  24269  lmiisolem  24365  elpreq  27626  xrge0nre  27917  esumcvgre  28323  eulerpartlemgvv  28582  ballotlem2  28694  eldmgm  28831  nofulllem5  29709  aomclem5  31246  cvgdvgrat  31438  bccbc  31494  elunnel1  31657  elunnel2  31658  stoweidlem26  32050  stoweidlem34  32058  fourierswlem  32255  lclkrlem2h  37657
  Copyright terms: Public domain W3C validator