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
Assertion
Ref Expression
orcanai

Proof of Theorem orcanai
StepHypRef Expression
1 orcanai.1 . . 3
21ord 368 . 2
32imp 420 1
 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