Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > orcanai | Structured version Visualization version Unicode version |
Description: Change disjunction in consequent to conjunction in antecedent. (Contributed by NM, 8-Jun-1994.) |
Ref | Expression |
---|---|
orcanai.1 |
Ref | Expression |
---|---|
orcanai |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orcanai.1 | . . 3 | |
2 | 1 | ord 392 | . 2 |
3 | 2 | imp 445 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wi 4 wo 383 wa 384 |
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 197 df-or 385 df-an 386 |
This theorem is referenced by: elunnel1 3754 bren2 7986 php 8144 unxpdomlem3 8166 tcrank 8747 dfac12lem1 8965 dfac12lem2 8966 ttukeylem3 9333 ttukeylem5 9335 ttukeylem6 9336 xrmax2 12007 xrmin1 12008 xrge0nre 12277 ccatco 13581 pcgcd 15582 mreexexd 16308 tsrlemax 17220 gsumval2 17280 xrsdsreval 19791 xrsdsreclb 19793 xrsxmet 22612 elii2 22735 xrhmeo 22745 pcoass 22824 limccnp 23655 logreclem 24500 eldmgm 24748 lgsdir2 25055 colmid 25583 lmiisolem 25688 elpreq 29360 esumcvgre 30153 eulerpartlemgvv 30438 ballotlem2 30550 lclkrlem2h 36803 aomclem5 37628 cvgdvgrat 38512 bccbc 38544 elunnel2 39198 stoweidlem26 40243 stoweidlem34 40251 fourierswlem 40447 |
Copyright terms: Public domain | W3C validator |