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

Theorem orcanai 897
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 377 . 2  |-  ( ph  ->  ( -.  ps  ->  ch ) )
32imp 429 1  |-  ( (
ph  /\  -.  ps )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 368    /\ wa 369
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 370  df-an 371
This theorem is referenced by:  bren2  7328  php  7483  unxpdomlem3  7507  tcrank  8079  dfac12lem1  8300  dfac12lem2  8301  ttukeylem3  8668  ttukeylem5  8670  ttukeylem6  8671  xrmax2  11136  xrmin1  11137  ccatcl  12258  ccatco  12447  pcgcd  13927  tsrlemax  15373  gsumval2  15493  xrsdsreval  17702  xrsdsreclb  17704  xrsxmet  20228  elii2  20350  xrhmeo  20360  pcoass  20438  limccnp  21208  logreclem  22099  lgsdir2  22552  elpreq  25724  xrge0nre  25976  eulerpartlemgvv  26607  ballotlem2  26719  eldmgm  26856  nofulllem5  27694  aomclem5  29256  stoweidlem26  29667  stoweidlem34  29675  lclkrlem2h  34732
  Copyright terms: Public domain W3C validator