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

Theorem orcanai 921
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 378 . 2  |-  ( ph  ->  ( -.  ps  ->  ch ) )
32imp 430 1  |-  ( (
ph  /\  -.  ps )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 369    /\ wa 370
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 188  df-or 371  df-an 372
This theorem is referenced by:  elunnel1  3613  bren2  7607  php  7762  unxpdomlem3  7784  tcrank  8354  dfac12lem1  8571  dfac12lem2  8572  ttukeylem3  8939  ttukeylem5  8941  ttukeylem6  8942  xrmax2  11471  xrmin1  11472  ccatco  12917  pcgcd  14790  tsrlemax  16417  gsumval2  16474  xrsdsreval  18948  xrsdsreclb  18950  xrsxmet  21738  elii2  21860  xrhmeo  21870  pcoass  21948  limccnp  22723  logreclem  23564  eldmgm  23812  lgsdir2  24119  colmid  24590  lmiisolem  24694  elpreq  27995  xrge0nre  28291  esumcvgre  28751  eulerpartlemgvv  29035  ballotlem2  29147  nofulllem5  30380  lclkrlem2h  34790  aomclem5  35621  cvgdvgrat  36298  bccbc  36330  elunnel2  36999  stoweidlem26  37454  stoweidlem34  37463  fourierswlem  37661
  Copyright terms: Public domain W3C validator