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

Theorem orcanai 879
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 366 . 2  |-  ( ph  ->  ( -.  ps  ->  ch ) )
32imp 418 1  |-  ( (
ph  /\  -.  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 357    /\ wa 358
This theorem is referenced by:  bren2  6908  php  7061  unxpdomlem3  7085  tcrank  7570  dfac12lem1  7785  dfac12lem2  7786  ttukeylem3  8154  ttukeylem5  8156  ttukeylem6  8157  xrmax2  10521  xrmin1  10522  ccatcl  11445  ccatco  11506  pcgcd  12946  tsrlemax  14345  gsumval2  14476  xrsdsreval  16432  xrsdsreclb  16434  xrsxmet  18331  elii2  18450  xrhmeo  18460  pcoass  18538  limccnp  19257  logreclem  20132  lgsdir2  20583  eldmgm  23709  nofulllem5  24431  aomclem5  27258  stoweidlem26  27878  stoweidlem34  27886  lclkrlem2h  32326
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 177  df-or 359  df-an 360
  Copyright terms: Public domain W3C validator