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

Theorem orcanai 911
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  7543  php  7698  unxpdomlem3  7723  tcrank  8298  dfac12lem1  8519  dfac12lem2  8520  ttukeylem3  8887  ttukeylem5  8889  ttukeylem6  8890  xrmax2  11373  xrmin1  11374  ccatcl  12554  ccatco  12760  pcgcd  14256  tsrlemax  15703  gsumval2  15826  xrsdsreval  18231  xrsdsreclb  18233  xrsxmet  21049  elii2  21171  xrhmeo  21181  pcoass  21259  limccnp  22030  logreclem  22878  lgsdir2  23331  elpreq  27091  xrge0nre  27342  eulerpartlemgvv  27955  ballotlem2  28067  eldmgm  28204  nofulllem5  29043  aomclem5  30608  stoweidlem26  31326  stoweidlem34  31334  lclkrlem2h  36311
  Copyright terms: Public domain W3C validator