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

Theorem orcanai 904
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  7332  php  7487  unxpdomlem3  7511  tcrank  8083  dfac12lem1  8304  dfac12lem2  8305  ttukeylem3  8672  ttukeylem5  8674  ttukeylem6  8675  xrmax2  11140  xrmin1  11141  ccatcl  12266  ccatco  12455  pcgcd  13936  tsrlemax  15382  gsumval2  15504  xrsdsreval  17838  xrsdsreclb  17840  xrsxmet  20366  elii2  20488  xrhmeo  20498  pcoass  20576  limccnp  21346  logreclem  22194  lgsdir2  22647  elpreq  25868  xrge0nre  26121  eulerpartlemgvv  26728  ballotlem2  26840  eldmgm  26977  nofulllem5  27816  aomclem5  29382  stoweidlem26  29792  stoweidlem34  29800  lclkrlem2h  35052
  Copyright terms: Public domain W3C validator