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

Theorem orcanai 881
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 368 . 2  |-  ( ph  ->  ( -.  ps  ->  ch ) )
32imp 420 1  |-  ( (
ph  /\  -.  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 359    /\ wa 360
This theorem is referenced by:  bren2  7141  php  7294  unxpdomlem3  7318  tcrank  7813  dfac12lem1  8028  dfac12lem2  8029  ttukeylem3  8396  ttukeylem5  8398  ttukeylem6  8399  xrmax2  10769  xrmin1  10770  ccatcl  11748  ccatco  11809  pcgcd  13256  tsrlemax  14657  gsumval2  14788  xrsdsreval  16748  xrsdsreclb  16750  xrsxmet  18845  elii2  18966  xrhmeo  18976  pcoass  19054  limccnp  19783  logreclem  20665  lgsdir2  21117  elpreq  24004  xrge0nre  24218  ballotlem2  24751  eldmgm  24811  nofulllem5  25666  aomclem5  27147  stoweidlem26  27765  stoweidlem34  27773  lclkrlem2h  32386
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 179  df-or 361  df-an 362
  Copyright terms: Public domain W3C validator