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

Theorem orcanai 879
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 366 . 2  |-  ( ph  ->  ( -.  ps  ->  ch ) )
32imp 418 1  |-  ( (
ph  /\  -.  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 357    /\ wa 358
This theorem is referenced by:  bren2  6892  php  7045  unxpdomlem3  7069  tcrank  7554  dfac12lem1  7769  dfac12lem2  7770  ttukeylem3  8138  ttukeylem5  8140  ttukeylem6  8141  xrmax2  10505  xrmin1  10506  ccatcl  11429  ccatco  11490  pcgcd  12930  tsrlemax  14329  gsumval2  14460  xrsdsreval  16416  xrsdsreclb  16418  xrsxmet  18315  elii2  18434  xrhmeo  18444  pcoass  18522  limccnp  19241  logreclem  20116  lgsdir2  20567  eldmgm  23105  nofulllem5  23771  aomclem5  26567  stoweidlem26  27187  stoweidlem34  27195  lclkrlem2h  31077
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360
  Copyright terms: Public domain W3C validator