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  7076  php  7229  unxpdomlem3  7253  tcrank  7743  dfac12lem1  7958  dfac12lem2  7959  ttukeylem3  8326  ttukeylem5  8328  ttukeylem6  8329  xrmax2  10698  xrmin1  10699  ccatcl  11672  ccatco  11733  pcgcd  13180  tsrlemax  14581  gsumval2  14712  xrsdsreval  16668  xrsdsreclb  16670  xrsxmet  18713  elii2  18834  xrhmeo  18844  pcoass  18922  limccnp  19647  logreclem  20529  lgsdir2  20981  elpreq  23845  xrge0nre  24044  ballotlem2  24527  eldmgm  24587  nofulllem5  25386  aomclem5  26826  stoweidlem26  27445  stoweidlem34  27453  lclkrlem2h  31631
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