MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  orcanai Structured version   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  7130  php  7283  unxpdomlem3  7307  tcrank  7800  dfac12lem1  8015  dfac12lem2  8016  ttukeylem3  8383  ttukeylem5  8385  ttukeylem6  8386  xrmax2  10756  xrmin1  10757  ccatcl  11735  ccatco  11796  pcgcd  13243  tsrlemax  14644  gsumval2  14775  xrsdsreval  16735  xrsdsreclb  16737  xrsxmet  18832  elii2  18953  xrhmeo  18963  pcoass  19041  limccnp  19770  logreclem  20652  lgsdir2  21104  elpreq  23991  xrge0nre  24205  ballotlem2  24738  eldmgm  24798  nofulllem5  25653  aomclem5  27114  stoweidlem26  27732  stoweidlem34  27740  lclkrlem2h  32239
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