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

Theorem orcanai 880
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 367 . 2  |-  ( ph  ->  ( -.  ps  ->  ch ) )
32imp 419 1  |-  ( (
ph  /\  -.  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 358    /\ wa 359
This theorem is referenced by:  bren2  7097  php  7250  unxpdomlem3  7274  tcrank  7764  dfac12lem1  7979  dfac12lem2  7980  ttukeylem3  8347  ttukeylem5  8349  ttukeylem6  8350  xrmax2  10720  xrmin1  10721  ccatcl  11698  ccatco  11759  pcgcd  13206  tsrlemax  14607  gsumval2  14738  xrsdsreval  16698  xrsdsreclb  16700  xrsxmet  18793  elii2  18914  xrhmeo  18924  pcoass  19002  limccnp  19731  logreclem  20613  lgsdir2  21065  elpreq  23952  xrge0nre  24166  ballotlem2  24699  eldmgm  24759  nofulllem5  25574  aomclem5  27023  stoweidlem26  27642  stoweidlem34  27650  lclkrlem2h  31997
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361
  Copyright terms: Public domain W3C validator